# HG changeset patch
# User nipkow
# Date 968253428 -7200
# Node ID b2a62260f8ace45169b5f0ef23ef02a642bb9ce8
# Parent  a069795f106017e6a74cda248d465acfdadfa8a6
less_induct -> nat_less_induct

diff -r a069795f1060 -r b2a62260f8ac src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Sep 06 16:54:12 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Sep 06 17:17:08 2000 +0200
@@ -695,7 +695,7 @@
 by (res_inst_tac [("x","schB")] spec 1);
 by (res_inst_tac [("x","tr")] spec 1);
 by (thin_tac' 5 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (REPEAT (rtac allI 1));
 ren "tr schB schA" 1;
 by (strip_tac 1);
@@ -935,7 +935,7 @@
 by (res_inst_tac [("x","schB")] spec 1);
 by (res_inst_tac [("x","tr")] spec 1);
 by (thin_tac' 5 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (REPEAT (rtac allI 1));
 ren "tr schB schA" 1;
 by (strip_tac 1);
diff -r a069795f1060 -r b2a62260f8ac src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Sep 06 16:54:12 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Sep 06 17:17:08 2000 +0200
@@ -945,7 +945,7 @@
          important, as otherwise either (Forall Q s1) would be in the IH as
          assumption (then rule useless) or it is not possible to strengthen 
          the IH by doing a forall closure of the sequence t (then rule also useless).
-         This is also the reason why the induction rule (less_induct or nat_induct) has to 
+         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to 
          to be imbuilt into the rule, as induction has to be done early and the take lemma 
          has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
 
@@ -983,7 +983,7 @@
 by (rtac mp 1);
 by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
@@ -1037,7 +1037,7 @@
 by (res_inst_tac [("x","h2a")] spec 1);
 by (res_inst_tac [("x","h1a")] spec 1);
 by (res_inst_tac [("x","x")] spec 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
@@ -1064,7 +1064,7 @@
 
 FIX
 
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (claset() addSIs [seq_take_lemma RS iffD2 RS spec],
diff -r a069795f1060 -r b2a62260f8ac src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed Sep 06 16:54:12 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed Sep 06 17:17:08 2000 +0200
@@ -160,7 +160,7 @@
 by (assume_tac 2);
 by (thin_tac' 1 1);
 by (res_inst_tac [("x","s")] spec 1);
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
 by (strip_tac 1);
 ren "na n s" 1;
 by (case_tac "Forall (%x. ~ P x) s" 1);