equal
deleted
inserted
replaced
69 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
69 case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts, |
70 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } |
70 simps=SOME simps, inducts=SOME inducts, termination=termination, eqvts=teqvts } |
71 in |
71 in |
72 (info', |
72 (info', |
73 lthy |
73 lthy |
74 |> Local_Theory.declaration false (add_function_data o morph_function_data info') |
74 |> Local_Theory.declaration {syntax = false, pervasive = false} |
|
75 (add_function_data o morph_function_data info') |
75 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
76 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)) |
76 end) |
77 end) |
77 end |
78 end |
78 in |
79 in |
79 (goal, afterqed, termination) |
80 (goal, afterqed, termination) |