equal
deleted
inserted
replaced
181 |
181 |
182 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
182 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info) |
183 val eqn_thms = |
183 val eqn_thms = |
184 (message ("Proving equations for primrec function " ^ fname); |
184 (message ("Proving equations for primrec function " ^ fname); |
185 eqn_terms |> map (fn t => |
185 eqn_terms |> map (fn t => |
186 standard (Goal.prove thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
186 Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
187 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])))); |
187 (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1]))); |
188 |
188 |
189 val (eqn_thms', thy2) = |
189 val (eqn_thms', thy2) = |
190 thy1 |
190 thy1 |
191 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
191 |> PureThy.add_thms ((eqn_names ~~ eqn_thms) ~~ eqn_atts); |
192 val (_, thy3) = |
192 val (_, thy3) = |