--- a/src/ZF/pair.thy Fri May 13 22:55:00 2011 +0200
+++ b/src/ZF/pair.thy Fri May 13 23:24:06 2011 +0200
@@ -1,7 +1,6 @@
(* Title: ZF/pair.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
-
*)
header{*Ordered Pairs*}
@@ -10,6 +9,14 @@
uses "simpdata.ML"
begin
+declaration {*
+ fn _ => Simplifier.map_ss (fn ss =>
+ ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
+ addcongs [@{thm if_weak_cong}])
+*}
+
+ML {* val ZF_ss = @{simpset} *}
+
simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
let
val unfold_bex_tac = unfold_tac @{thms Bex_def};