# HG changeset patch
# User nipkow
# Date 861900674 -7200
# Node ID 3e3087aa69e7c4888c169615f9a918eb8d3e0736
# Parent  63a77d6b7eca8ed8c9e19302129c91924d351fda
Updates because nat_ind_tac no longer appends "1" to the ind.var.

diff -r 63a77d6b7eca -r 3e3087aa69e7 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu Apr 24 18:44:32 1997 +0200
+++ b/src/HOLCF/Fix.ML	Thu Apr 24 18:51:14 1997 +0200
@@ -199,8 +199,8 @@
         (nat_ind_tac "n" 1),
         (Simp_tac 1),
         (Simp_tac 1),
-        (res_inst_tac [("t","iterate n1 F (lub(range(%u. Y u)))"),
-        ("s","lub(range(%i. iterate n1 F (Y i)))")] ssubst 1),
+        (res_inst_tac [("t","iterate n F (lub(range(%u. Y u)))"),
+        ("s","lub(range(%i. iterate n F (Y i)))")] ssubst 1),
         (atac 1),
         (rtac contlub_cfun_arg 1),
         (etac (monofun_iterate2 RS ch2ch_monofun) 1)
diff -r 63a77d6b7eca -r 3e3087aa69e7 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:44:32 1997 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Apr 24 18:51:14 1997 +0200
@@ -442,7 +442,7 @@
                                   asm_simp_tac take_ss 1 ::
                                   map (fn arg =>
                                    case_UU_tac (prems@con_rews) 1 (
-                           nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
+                           nth_elem(rec_of arg,dnames)^"_take n`"^vname arg))
                                   (filter is_nonlazy_rec args) @ [
                                   resolve_tac prems 1] @
                                   map (K (atac 1))      (nonlazy args) @
diff -r 63a77d6b7eca -r 3e3087aa69e7 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Thu Apr 24 18:44:32 1997 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Thu Apr 24 18:51:14 1997 +0200
@@ -130,10 +130,10 @@
         (Simp_tac 1),
         (Simp_tac 1),
         (strip_tac 1),
-        (res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
+        (res_inst_tac [("s","p`(iterate k g x)")] trans 1),
         (rtac trans 1),
         (rtac (p_def3 RS sym) 2),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
         (rtac mp 1),
         (etac spec 1),
         (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
@@ -145,7 +145,7 @@
         (etac less_trans 1),
         (Simp_tac 1)
         ]);
-trace_simp := false;
+
 val hoare_lemma24 = prove_goal Hoare.thy 
 "(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \
 \ q`(iterate k g x)=q`x"
@@ -155,10 +155,10 @@
         (Simp_tac 1),
 (simp_tac (!simpset addsimps [less_Suc_eq]) 1),
         (strip_tac 1),
-        (res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
+        (res_inst_tac [("s","q`(iterate k g x)")] trans 1),
         (rtac trans 1),
         (rtac (q_def3 RS sym) 2),
-        (res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
+        (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
         (fast_tac HOL_cs 1),
         (simp_tac HOLCF_ss 1),
         (etac mp 1),
diff -r 63a77d6b7eca -r 3e3087aa69e7 src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Thu Apr 24 18:44:32 1997 +0200
+++ b/src/HOLCF/ex/Loop.ML	Thu Apr 24 18:51:14 1997 +0200
@@ -120,7 +120,7 @@
         (Asm_simp_tac 1),
         (strip_tac 1),
         (simp_tac (!simpset addsimps [step_def2]) 1),
-        (res_inst_tac [("p","b`(iterate k1 (step`b`g) x)")] trE 1),
+        (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1),
         (etac notE 1),
         (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
         (asm_simp_tac HOLCF_ss 1),
@@ -128,8 +128,8 @@
         (etac spec 1),
         (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
                                 addsimps [loop_lemma2] ) 1),
-        (res_inst_tac [("s","iterate (Suc k1) (step`b`g) x"),
-                ("t","g`(iterate k1 (step`b`g) x)")] ssubst 1),
+        (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
+                ("t","g`(iterate k (step`b`g) x)")] ssubst 1),
         (atac 2),
         (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
         (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]