src/ZF/QPair.ML

-(*  Title: 	ZF/QPair.ML
+(*  Title:      ZF/QPair.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 For QPair.thy.  
 
 Quine-inspired ordered pairs and disjoint sums, for non-well-founded data

 
 (** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
 
 val QSigmaE2 = 
   rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
-		  THEN prune_params_tac)
+                  THEN prune_params_tac)
       (read_instantiate [("c","<a;b>")] QSigmaE);  
 
 qed_goal "QSigmaD1" thy "<a;b> : QSigma(A,B) ==> a : A"
  (fn [major]=>
   [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);

 goalw thy [qsplit_def] "!!R a b. R(a,b) ==> qsplit(R, <a;b>)";
 by (asm_simp_tac qpair_ss 1);
 qed "qsplitI";
 
 val major::sigma::prems = goalw thy [qsplit_def]
-    "[| qsplit(R,z);  z:QSigma(A,B);  			\
-\       !!x y. [| z = <x;y>;  R(x,y) |] ==> P  		\
+    "[| qsplit(R,z);  z:QSigma(A,B);                    \
+\       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
 \   |] ==> P";
 by (rtac (sigma RS QSigmaE) 1);
 by (cut_facts_tac [major] 1);
 by (asm_full_simp_tac (qpair_ss addsimps prems) 1);
 qed "qsplitE";

     (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
     (hyp_subst_tac 1),
     (assume_tac 1) ]);
 
 val qconverse_cs = qpair_cs addSIs [qconverseI] 
-			    addSEs [qconverseD,qconverseE];
+                            addSEs [qconverseD,qconverseE];
 
 qed_goal "qconverse_qconverse" thy
     "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
  (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
 

 \       !!y. y: B ==> d(y): C(QInr(y)) \
 \    |] ==> qcase(c,d,u) : C(u)";
 by (rtac (major RS qsumE) 1);
 by (ALLGOALS (etac ssubst));
 by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
-			    (prems@[qcase_QInl,qcase_QInr]))));
+                            (prems@[qcase_QInl,qcase_QInr]))));
 qed "qcase_type";
 
 (** Rules for the Part primitive **)
 
 goal thy "Part(A <+> B,QInl) = {QInl(x). x: A}";