translate anub (required MEMBER_INTRO for the induction thm)

CakeML · Apr 22, 2015 · db1927b · db1927b
1 parent 0993b6e
commit db1927b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/bootstrap/translation/repl/replMLScript.sml b/bootstrap/translation/repl/replMLScript.sml
@@ -282,9 +282,11 @@ val ts_unify_side_def = store_thm("ts_unify_side_def",
   THEN FULL_SIMP_TAC std_ss [])
   |> update_precondition;
 
-
 (* type inference: rest *)
 
+val _ = save_thm("anub_ind",REWRITE_RULE[MEMBER_INTRO]miscTheory.anub_ind)
+val _ = translate (REWRITE_RULE[MEMBER_INTRO] miscTheory.anub_def)
+
 val _ = (extra_preprocessing :=
   [MEMBER_INTRO, MAP, OPTION_BIND_THM, st_ex_bind_def,
    st_ex_return_def, failwith_def, guard_def, read_def, write_def]);