less_induct -> nat_less_induct

--- 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);

--- 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],

--- 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);