equal
deleted
inserted
replaced
35 open FundefCommon |
35 open FundefCommon |
36 |
36 |
37 val simp_attribs = map (Attrib.internal o K) |
37 val simp_attribs = map (Attrib.internal o K) |
38 [Simplifier.simp_add, |
38 [Simplifier.simp_add, |
39 Code.add_default_eqn_attribute, |
39 Code.add_default_eqn_attribute, |
40 Nitpick_Const_Simps.add, |
40 Nitpick_Simps.add, |
41 Quickcheck_RecFun_Simps.add] |
41 Quickcheck_RecFun_Simps.add] |
42 |
42 |
43 val psimp_attribs = map (Attrib.internal o K) |
43 val psimp_attribs = map (Attrib.internal o K) |
44 [Simplifier.simp_add, |
44 [Simplifier.simp_add, |
45 Nitpick_Const_Psimps.add] |
45 Nitpick_Psimps.add] |
46 |
46 |
47 fun note_theorem ((name, atts), ths) = |
47 fun note_theorem ((name, atts), ths) = |
48 LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) |
48 LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths) |
49 |
49 |
50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |
50 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_" |