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