equal
deleted
inserted
replaced
23 open Function_Common |
23 open Function_Common |
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 Code.Equation, |
29 Named_Theorems.add @{named_theorems nitpick_simp}] |
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 = |