Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/set_comprehension_pointfree.ML
changeset 49942 50e457bbc5fe
parent 49901 58cac1b3b535
child 49943 6a26fed71755 
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Fri Oct 19 21:52:45 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 18 10:06:27 2012 +0200
@@ -352,7 +352,8 @@
 
 (* main simprocs *)
 
-val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
+val prep_thms =
+  map mk_meta_eq ([@{thm Bex_def}, @{thm Pow_iff[symmetric]}] @ @{thms ex_simps[symmetric]})
 
 val post_thms =
   map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},
isabelle