fixed var index in tactic;
authorwenzelm
Thu Jul 28 15:19:48 2005 +0200 (2005-07-28)
changeset 1693391ded127f5f7
parent 16932 0bca871f5a21
child 16934 9ef19e3c7fdd
fixed var index in tactic;
src/HOL/Matrix/MatrixGeneral.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Thu Jul 28 15:19:47 2005 +0200
     1.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Thu Jul 28 15:19:48 2005 +0200
     1.3 @@ -1058,7 +1058,7 @@
     1.4      apply (induct n)
     1.5      apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
     1.6      apply (auto)
     1.7 -    by (drule_tac x3="(% j i. A j (Suc i))" in forall, simp)
     1.8 +    by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
     1.9    show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
    1.10      apply (simp add: foldmatrix_def foldmatrix_transposed_def)
    1.11      apply (induct m, simp)
     2.1 --- a/src/HOLCF/Up.thy	Thu Jul 28 15:19:47 2005 +0200
     2.2 +++ b/src/HOLCF/Up.thy	Thu Jul 28 15:19:48 2005 +0200
     2.3 @@ -114,7 +114,7 @@
     2.4  lemma up_lemma6:
     2.5    "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk>  
     2.6        \<Longrightarrow> range Y <<| Iup (\<Squnion>i. THE a. Iup a = Y(i + j))"
     2.7 -apply (rule_tac j1="j" in is_lub_range_shift [THEN iffD1])
     2.8 +apply (rule_tac j1 = j in is_lub_range_shift [THEN iffD1])
     2.9  apply assumption
    2.10  apply (subst up_lemma5, assumption+)
    2.11  apply (rule is_lub_Iup)