Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Matrix/MatrixGeneral.thy
changeset 16933 91ded127f5f7
parent 16417 9bc16273c2d4
child 20217 25b068a99d2b 
--- 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)
isabelle