equal
deleted
inserted
replaced
126 fs=fs, R=R, defname=defname, is_partial=true } |
126 fs=fs, R=R, defname=defname, is_partial=true } |
127 |
127 |
128 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
128 val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes) |
129 in |
129 in |
130 (info, |
130 (info, |
131 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
131 lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info)) |
132 end |
132 end |
133 in |
133 in |
134 ((goal_state, afterqed), lthy') |
134 ((goal_state, afterqed), lthy') |
135 end |
135 end |
136 |
136 |
201 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
201 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
202 simps=SOME simps, inducts=SOME inducts, termination=termination } |
202 simps=SOME simps, inducts=SOME inducts, termination=termination } |
203 in |
203 in |
204 (info', |
204 (info', |
205 lthy |
205 lthy |
206 |> Local_Theory.declaration false (add_function_data o morph_function_data info') |
206 |> Local_Theory.declaration false (add_function_data o transform_function_data info') |
207 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
207 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
208 end) |
208 end) |
209 end |
209 end |
210 in |
210 in |
211 (goal, afterqed, termination) |
211 (goal, afterqed, termination) |