# HG changeset patch
# User wenzelm
# Date 1122556788 -7200
# Node ID 91ded127f5f7e02f91803c2ed620cc14c1687cd5
# Parent  0bca871f5a21b4daa8d79d3855bff9466d53cb29
fixed var index in tactic;

diff -r 0bca871f5a21 -r 91ded127f5f7 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Jul 28 15:19:47 2005 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Jul 28 15:19:48 2005 +0200
@@ -1058,7 +1058,7 @@
     apply (induct n)
     apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
     apply (auto)
-    by (drule_tac x3="(% j i. A j (Suc i))" in forall, simp)
+    by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
   show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
     apply (simp add: foldmatrix_def foldmatrix_transposed_def)
     apply (induct m, simp)
diff -r 0bca871f5a21 -r 91ded127f5f7 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Thu Jul 28 15:19:47 2005 +0200
+++ b/src/HOLCF/Up.thy	Thu Jul 28 15:19:48 2005 +0200
@@ -114,7 +114,7 @@
 lemma up_lemma6:
   "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
       \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
-apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
+apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
 apply assumption
 apply (subst up_lemma5, assumption+)
 apply (rule is_lub_Iup)