# HG changeset patch
# User paulson
# Date 896264552 -7200
# Node ID 09b8945cac07ade9749bd1aeed5401c5d85ab2a4
# Parent  8b65444edbb00a167f19a962df405dfaf891f2b4
more tracing

diff -r 8b65444edbb0 -r 09b8945cac07 src/HOL/indrule.ML
--- a/src/HOL/indrule.ML	Wed May 27 12:21:39 1998 +0200
+++ b/src/HOL/indrule.ML	Wed May 27 12:22:32 1998 +0200
@@ -108,6 +108,11 @@
         ind_tac (rev prems) (length prems)])
     handle e => print_sign_exn sign e;
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln "quant_induct = "; print_thm quant_induct)
+        else ();
+
+
 (*** Prove the simultaneous induction rule ***)
 
 (*Make distinct predicates for each inductive set.
@@ -150,6 +155,14 @@
 and mutual_induct_concl = 
     Ind_Syntax.mk_Trueprop (fold_bal (app Ind_Syntax.conj) qconcls);
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln ("induct_concl = " ^
+		      Sign.string_of_term sign induct_concl);
+             writeln ("mutual_induct_concl = " ^
+		      Sign.string_of_term sign mutual_induct_concl))
+        else ();
+
+
 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
                         resolve_tac [allI, impI, conjI, Part_eqI, refl],
                         dresolve_tac [spec, mp, splitD]];
@@ -170,6 +183,11 @@
   else (writeln "  [ No mutual induction rule needed ]";
         TrueI);
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln "lemma = "; print_thm lemma)
+        else ();
+
+
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
 (*Simplification largely reduces the mutual induction rule to the 
diff -r 8b65444edbb0 -r 09b8945cac07 src/ZF/indrule.ML
--- a/src/ZF/indrule.ML	Wed May 27 12:21:39 1998 +0200
+++ b/src/ZF/indrule.ML	Wed May 27 12:22:32 1998 +0200
@@ -108,6 +108,11 @@
                            ORELSE' hyp_subst_tac)),
         ind_tac (rev prems) (length prems) ]);
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln "quant_induct = "; print_thm quant_induct)
+        else ();
+
+
 (*** Prove the simultaneous induction rule ***)
 
 (*Make distinct predicates for each inductive set*)
@@ -155,6 +160,14 @@
 and mutual_induct_concl =
  FOLogic.mk_Trueprop(fold_bal (app FOLogic.conj) qconcls);
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln ("induct_concl = " ^
+		      Sign.string_of_term sign induct_concl);
+             writeln ("mutual_induct_concl = " ^
+		      Sign.string_of_term sign mutual_induct_concl))
+        else ();
+
+
 val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
                         resolve_tac [allI, impI, conjI, Part_eqI],
                         dresolve_tac [spec, mp, Pr.fsplitD]];
@@ -174,6 +187,11 @@
   else (writeln "  [ No mutual induction rule needed ]";
         TrueI);
 
+val _ = if !Ind_Syntax.trace then 
+            (writeln "lemma = "; print_thm lemma)
+        else ();
+
+
 (*Mutual induction follows by freeness of Inl/Inr.*)
 
 (*Simplification largely reduces the mutual induction rule to the 
@@ -189,7 +207,8 @@
   where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
   Instead the following rules extract the relevant conjunct.
 *)
-val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos RLN (2,[rev_subsetD]);
+val cmonos = [subset_refl RS Collect_mono] RL Inductive.monos
+              RLN (2,[rev_subsetD]);
 
 (*Minimizes backtracking by delivering the correct premise to each goal*)
 fun mutual_ind_tac [] 0 = all_tac