src/ZF/upair.ML
 changeset 1461 6bcb44e4d6e5 parent 1017 6a402dc505cf child 1609 5324067d993f
```--- a/src/ZF/upair.ML	Mon Jan 29 14:16:13 1996 +0100
+++ b/src/ZF/upair.ML	Tue Jan 30 13:42:57 1996 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	ZF/upair
+(*  Title:      ZF/upair
ID:         \$Id\$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

UNORDERED pairs in Zermelo-Fraenkel Set Theory
@@ -14,9 +14,9 @@

(*** Lemmas about power sets  ***)

-val Pow_bottom = empty_subsetI RS PowI;		(* 0 : Pow(B) *)
-val Pow_top = subset_refl RS PowI;		(* A : Pow(A) *)
-val Pow_neq_0 = Pow_top RSN (2,equals0D);	(* Pow(a)=0 ==> P *)
+val Pow_bottom = empty_subsetI RS PowI;         (* 0 : Pow(B) *)
+val Pow_top = subset_refl RS PowI;              (* A : Pow(A) *)
+val Pow_neq_0 = Pow_top RSN (2,equals0D);       (* Pow(a)=0 ==> P *)

(*** Unordered pairs - Upair ***)
@@ -176,7 +176,7 @@
"[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
(fn [pa,eq] =>
-	                 addEs [eq RS subst]) 1) ]);
+                         addEs [eq RS subst]) 1) ]);

(* Only use this if you already know EX!x. P(x) *)
qed_goal "the_equality2" ZF.thy
@@ -194,8 +194,8 @@
qed_goal "theI2" ZF.thy
"[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
(fn prems => [ resolve_tac prems 1,
-	        rtac theI 1,
-		resolve_tac prems 1 ]);
+                rtac theI 1,
+                resolve_tac prems 1 ]);

(*the_cong is no longer necessary: if (ALL y.P(y)<->Q(y)) then
(THE x.P(x))  rewrites to  (THE x. Q(x))  *)
@@ -238,8 +238,8 @@
qed_goal "expand_if" ZF.thy
"P(if(Q,x,y)) <-> ((Q --> P(x)) & (~Q --> P(y)))"
(fn _=> [ (excluded_middle_tac "Q" 1),
-	   (asm_simp_tac if_ss 1),
-	   (asm_simp_tac if_ss 1) ]);
+           (asm_simp_tac if_ss 1),
+           (asm_simp_tac if_ss 1) ]);

qed_goal "if_iff" ZF.thy "a: if(P,x,y) <-> P & a:x | ~P & a:y"
(fn _=> [ (simp_tac (if_ss setloop split_tac [expand_if]) 1) ]);
@@ -247,7 +247,7 @@
qed_goal "if_type" ZF.thy
"[| P ==> a: A;  ~P ==> b: A |] ==> if(P,a,b): A"
(fn prems=> [ (simp_tac
-		(if_ss addsimps prems setloop split_tac [expand_if]) 1) ]);
+                (if_ss addsimps prems setloop split_tac [expand_if]) 1) ]);

(*** Foundation lemmas ***)
@@ -259,7 +259,7 @@
(etac equals0D 1),
(rtac consI1 1),