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.
Simplifier.cong_add_global;
authorwenzelm
Tue, 29 Aug 2000 00:55:59 +0200
changeset 9714 79db0e5b7824
parent 9713 2c5b42311eb0
child 9715 5705a04d24ea
Simplifier.cong_add_global;
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:31 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:59 2000 +0200
@@ -562,7 +562,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), [cong_add_global])]) |>
+        (("", weak_case_congs), [Simplifier.cong_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path |>
isabelle