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.
(intermediate commit)
authorhaftmann
Mon, 04 Jul 2005 11:04:10 +0200
changeset 16672 f83f3aef274d
parent 16671 ca316edcb031
child 16673 6b14aba5ddaa
(intermediate commit)
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_package.ML	Sat Jul 02 13:08:28 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Jul 04 11:04:10 2005 +0200
@@ -286,10 +286,10 @@
   (#1 o PureThy.add_thmss [(("simps", simps), []),
     (("", List.concat case_thms @ size_thms @ 
           List.concat distinct  @ rec_thms), [Simplifier.simp_add_global]),
-    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+    (("", size_thms @ rec_thms),             [RecfunCodegen.add NONE]),
     (("", List.concat inject),               [iff_add_global]),
     (("", List.concat distinct RL [notE]),   [Classical.safe_elim_global]),
-    (("", weak_case_congs),           [cong_att])]);
+    (("", weak_case_congs),                  [cong_att])]);
 
 
 (* add_cases_induct *)
isabelle