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.
removed "nitpick_const_simp" attribute from Record's "simps";
authorblanchet
Wed, 21 Oct 2009 16:53:00 +0200
changeset 33053 dabf9d1bb552
parent 32956 c39860141415
child 33054 dd1192a96968
removed "nitpick_const_simp" attribute from Record's "simps"; Nitpick has its own notion of a record and doesn't need those.
src/HOL/Tools/record.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/record.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/HOL/Tools/record.ML	Wed Oct 21 16:53:00 2009 +0200
@@ -2362,8 +2362,7 @@
     val final_thy =
       thms_thy
       |> (snd oo PureThy.add_thmss)
-          [((Binding.name "simps", sel_upd_simps),
-            [Simplifier.simp_add, Nitpick_Const_Simps.add]),
+          [((Binding.name "simps", sel_upd_simps), [Simplifier.simp_add]),
            ((Binding.name "iffs", iffs), [iff_add])]
       |> put_record name (make_record_info args parent fields extension induct_scheme' ext_def)
       |> put_sel_upd names full_moreN depth sel_upd_simps sel_upd_defs (fold_congs', unfold_congs')
isabelle