# HG changeset patch
# User nipkow
# Date 908552023 -7200
# Node ID f8389824189b83e4529eebc4a9097f34b70a7196
# Parent  afd75136b236358783de416b4a824852d79e1770
Mods because trans_tac is now part of thge simplifier.

diff -r afd75136b236 -r f8389824189b src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Oct 16 17:32:29 1998 +0200
+++ b/src/HOLCF/Fix.ML	Fri Oct 16 17:33:43 1998 +0200
@@ -693,13 +693,7 @@
   val adm_disj_lemma4 = prove_goal Nat.thy
   "!!Q. !j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
  (fn _ =>
-        [
-        Asm_simp_tac 1,
-        strip_tac 1,
-        etac allE 1,
-        etac mp 1,
-        trans_tac 1
-        ]);
+        [Asm_simp_tac 1]);
 
   val adm_disj_lemma5 = prove_goal thy
   "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
diff -r afd75136b236 -r f8389824189b src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Oct 16 17:32:29 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Oct 16 17:33:43 1998 +0200
@@ -37,7 +37,6 @@
 
 goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
-by (Blast_tac 1);
 qed "pred_suc";