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.
to_set now applies collect_mem_simproc as well.
authorberghofe
Wed, 28 Nov 2007 14:56:38 +0100
changeset 25487 d96d5808d926
parent 25486 b944ef973109
child 25488 c945521fa0d9
to_set now applies collect_mem_simproc as well.
src/HOL/Tools/inductive_set_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Nov 28 09:01:50 2007 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Nov 28 14:56:38 2007 +0100
@@ -371,7 +371,7 @@
     thm |>
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
-        addsimprocs [strong_ind_simproc pred_arities]) |>
+        addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
     RuleCases.save thm
   end;
isabelle