equal
deleted
inserted
replaced
99 val termination_cmd = gen_termination Syntax.read_term |
99 val termination_cmd = gen_termination Syntax.read_term |
100 |
100 |
101 (* outer syntax *) |
101 (* outer syntax *) |
102 |
102 |
103 val option_parser = |
103 val option_parser = |
104 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! |
104 (Scan.optional (@{keyword "("} |-- Parse.!!! |
105 ((Parse.reserved "eqvt" >> K (true, true)) || |
105 ((Parse.reserved "eqvt" >> K (true, true)) || |
106 (Parse.reserved "no_eqvt" >> K (true, false))) --| Parse.$$$ ")") (false, false)) |
106 (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false)) |
107 |
107 |
108 val _ = |
108 val _ = |
109 Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function" |
109 Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) |
110 Keyword.thy_goal |
110 "prove termination of a recursive function" |
111 (option_parser -- Scan.option Parse.term >> |
111 (option_parser -- Scan.option Parse.term >> |
112 (fn ((is_nominal, is_eqvt), opt_trm) => |
112 (fn ((is_nominal, is_eqvt), opt_trm) => |
113 if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm)) |
113 if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm)) |
114 |
114 |
115 end |
115 end |