equal
deleted
inserted
replaced
104 (Scan.optional (@{keyword "("} |-- 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))) --| @{keyword ")"}) (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", Keyword.thy_goal) |
109 Outer_Syntax.local_theory_to_proof @{command_spec "termination"} |
110 "prove termination of a recursive function" |
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 |