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.
use cong_add_global att;
authorwenzelm
Fri, 31 Mar 2000 22:39:39 +0200
changeset 8645 40036a2ab646
parent 8644 c47735e7bd1c
child 8646 1a2c5ccebfdb
use cong_add_global att;
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_package.ML	Fri Mar 31 22:39:06 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 31 22:39:39 2000 +0200
@@ -529,7 +529,7 @@
       (#1 o PureThy.add_thmss [(("simps", simps), []),
         (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
         (("", flat (inject @ distinct)), [iff_add_global]),
-        (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
+        (("", weak_case_congs), [cong_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;
isabelle