src/ZF/simpdata.ML
 changeset 533 7357160bc56a parent 516 1957113f0d7d child 762 1cf9ebcc3ff3
```--- 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 \$ _)) = ```