equal
deleted
inserted
replaced
24 open Nominal_Function_Common |
24 open Nominal_Function_Common |
25 |
25 |
26 val simp_attribs = map (Attrib.internal o K) |
26 val simp_attribs = map (Attrib.internal o K) |
27 [Simplifier.simp_add, |
27 [Simplifier.simp_add, |
28 Code.add_default_eqn_attribute, |
28 Code.add_default_eqn_attribute, |
29 Nitpick_Simps.add] |
29 Named_Theorems.add @{named_theorems nitpick_simp}] |
30 |
30 |
31 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
31 val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add) |
32 |
32 |
33 fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy = |
33 fun prepare_termination_proof prep_term is_eqvt raw_term_opt lthy = |
34 let |
34 let |
105 (Scan.optional (@{keyword "("} |-- Parse.!!! |
105 (Scan.optional (@{keyword "("} |-- Parse.!!! |
106 ((Parse.reserved "eqvt" >> K true) || |
106 ((Parse.reserved "eqvt" >> K true) || |
107 (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (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 "nominal_termination"} |
110 Outer_Syntax.local_theory_to_proof @{command_keyword nominal_termination} |
111 "prove termination of a recursive nominal 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_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm)) |
113 (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm)) |
114 |
114 |
115 end |
115 end |