src/ZF/indrule.ML

--- a/src/ZF/indrule.ML	Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/indrule.ML	Thu Sep 26 15:14:23 1996 +0200
@@ -83,8 +83,8 @@
 val min_ss = empty_ss
       setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
       setsolver  (fn prems => resolve_tac (triv_rls@prems) 
-			      ORELSE' assume_tac
-			      ORELSE' etac FalseE);
+                              ORELSE' assume_tac
+                              ORELSE' etac FalseE);
 
 val quant_induct = 
     prove_goalw_cterm part_rec_defs 
@@ -118,13 +118,13 @@
 fun mk_predpair rec_tm = 
   let val rec_name = (#1 o dest_Const o head_of) rec_tm
       val pfree = Free(pred_name ^ "_" ^ rec_name,
-		       elem_factors ---> Ind_Syntax.oT)
+                       elem_factors ---> Ind_Syntax.oT)
       val qconcl = 
         foldr Ind_Syntax.mk_all 
-	  (elem_frees, 
-	   Ind_Syntax.imp $ 
-	   (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
-	         $ (list_comb (pfree, elem_frees)))
+          (elem_frees, 
+           Ind_Syntax.imp $ 
+           (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
+                 $ (list_comb (pfree, elem_frees)))
   in  (CP.ap_split elem_type Ind_Syntax.oT pfree, 
        qconcl)  
   end;
@@ -141,15 +141,15 @@
     Ind_Syntax.mk_tprop
       (Ind_Syntax.mk_all_imp
        (big_rec_tm,
-	Abs("z", Ind_Syntax.iT, 
-	    fold_bal (app Ind_Syntax.conj) 
-	    (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+        Abs("z", Ind_Syntax.iT, 
+            fold_bal (app Ind_Syntax.conj) 
+            (map mk_rec_imp (Inductive.rec_tms~~preds)))))
 and mutual_induct_concl =
  Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
 
 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
-			resolve_tac [allI, impI, conjI, Part_eqI],
-			dresolve_tac [spec, mp, Pr.fsplitD]];
+                        resolve_tac [allI, impI, conjI, Part_eqI],
+                        dresolve_tac [spec, mp, Pr.fsplitD]];
 
 val lemma = (*makes the link between the two induction rules*)
     prove_goalw_cterm part_rec_defs 
@@ -157,7 +157,7 @@
           (fn prems =>
            [cut_facts_tac prems 1, 
             REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
-		    lemma_tac 1)]);
+                    lemma_tac 1)]);
 
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
@@ -190,10 +190,10 @@
            IF_UNSOLVED (*simp_tac may have finished it off!*)
              ((*simplify assumptions*)
               (*some risk of excessive simplification here -- might have
-	        to identify the bare minimum set of rewrites*)
+                to identify the bare minimum set of rewrites*)
               full_simp_tac 
-	         (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
-	      THEN
+                 (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
+              THEN
               (*unpackage and use "prem" in the corresponding place*)
               REPEAT (rtac impI 1)  THEN
               rtac (rewrite_rule all_defs prem) 1  THEN
@@ -225,7 +225,7 @@
 val inst = 
     case elem_frees of [_] => I
        | _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)), 
-				 cterm_of sign elem_tuple)]);
+                                 cterm_of sign elem_tuple)]);
 
 (*strip quantifier and the implication*)
 val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
@@ -236,8 +236,8 @@
   (*strip quantifier*)
   val induct = standard 
                   (CP.split_rule_var
-		    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
-		     induct0));
+                    (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
+                     induct0));
 
   (*Just "True" unless there's true mutual recursion.  This saves storage.*)
   val mutual_induct =