# HG changeset patch
# User lcp
# Date 777056486 -7200
# Node ID 7357160bc56ab307a72e5f36482f64bb4b0d6f41
# Parent  851df239ac8b7dffd07408917bc1967d83e5a22f
ZF/pair.ML: moved some definitions here from simpdata.ML

diff -r 851df239ac8b -r 7357160bc56a src/ZF/pair.ML
--- a/src/ZF/pair.ML	Tue Aug 16 18:58:42 1994 +0200
+++ b/src/ZF/pair.ML	Tue Aug 16 19:01:26 1994 +0200
@@ -154,3 +154,30 @@
     addSEs [SigmaE2, SigmaE, Pair_inject, make_elim succ_inject,
 	    Pair_neq_0, sym RS Pair_neq_0, succ_neq_0, sym RS succ_neq_0];
 
+
+(*** Basic simplification for ZF; see simpdata.ML for full version ***)
+
+fun prove_fun s = 
+    (writeln s;  prove_goal ZF.thy s
+       (fn prems => [ (cut_facts_tac prems 1), (fast_tac pair_cs 1) ]));
+
+(*INCLUDED IN ZF_ss*)
+val mem_simps = map prove_fun
+ [ "a : 0             <-> False",
+   "a : A Un B        <-> a:A | a:B",
+   "a : A Int B       <-> a:A & a:B",
+   "a : A-B           <-> a:A & ~a:B",
+   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
+   "a : Collect(A,P)  <-> a:A & P(a)" ];
+
+goal ZF.thy "{x.x:A} = A";
+by (fast_tac (pair_cs addSIs [equalityI]) 1);
+val triv_RepFun = result();
+
+(*INCLUDED: should be??*)
+val bquant_simps = map prove_fun
+ [ "(ALL x:0.P(x)) <-> True",
+   "(EX  x:0.P(x)) <-> False",
+   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
+   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
+
diff -r 851df239ac8b -r 7357160bc56a src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Aug 16 18:58:42 1994 +0200
+++ b/src/ZF/simpdata.ML	Tue Aug 16 19:01:26 1994 +0200
@@ -6,30 +6,6 @@
 Rewriting for ZF set theory -- based on FOL rewriting
 *)
 
-fun prove_fun s = 
-    (writeln s;  prove_goal ZF.thy s
-       (fn prems => [ (cut_facts_tac prems 1), (fast_tac ZF_cs 1) ]));
-
-(*INCLUDED IN ZF_ss*)
-val mem_simps = map prove_fun
- [ "a : 0             <-> False",
-   "a : A Un B        <-> a:A | a:B",
-   "a : A Int B       <-> a:A & a:B",
-   "a : A-B           <-> a:A & ~a:B",
-   "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
-   "a : Collect(A,P)  <-> a:A & P(a)" ];
-
-goal ZF.thy "{x.x:A} = A";
-by (fast_tac eq_cs 1);
-val triv_RepFun = result();
-
-(*INCLUDED: should be??*)
-val bquant_simps = map prove_fun
- [ "(ALL x:0.P(x)) <-> True",
-   "(EX  x:0.P(x)) <-> False",
-   "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
-   "(EX  x:succ(i).P(x)) <-> P(i) | (EX  x:i.P(x))" ];
-
 (** Tactics for type checking -- from CTT **)
 
 fun is_rigid_elem (Const("Trueprop",_) $ (Const("op :",_) $ a $ _)) =