90 [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
90 [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd |
91 |> Proof_Context.note_thmss "" |
91 |> Proof_Context.note_thmss "" |
92 [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
92 [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd |
93 |> Proof_Context.note_thmss "" |
93 |> Proof_Context.note_thmss "" |
94 [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
94 [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]), |
95 [([Goal.norm_result termination], [])])] |> snd |
95 [([Goal.norm_result lthy termination], [])])] |> snd |
96 |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] |
96 |> Proof.theorem NONE (snd oo afterqed) [[(goal, [])]] |
97 end |
97 end |
98 |
98 |
99 val termination = gen_termination Syntax.check_term |
99 val termination = gen_termination Syntax.check_term |
100 val termination_cmd = gen_termination Syntax.read_term |
100 val termination_cmd = gen_termination Syntax.read_term |