Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorblanchet
Wed, 04 Mar 2009 15:33:07 +0100
changeset 30252 35518956f0ee
parent 30250 05d312f09a25 (current diff)
parent 30251 7aec011818e0 (diff)
child 30253 63cae7fd7e64
merged
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 14:23:54 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Mar 04 15:33:07 2009 +0100
@@ -374,7 +374,9 @@
          in
            lthy''
            |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
-             [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
+              (map (Attrib.internal o K)
+                   [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add],
+               maps snd simps')
            |> snd
          end)
       [goals] |>
isabelle