src/HOL/Matrix/Matrix.thy
changeset 32960 69916a850301
parent 32491 d5d8bea0cd94
child 33657 a4179bf442d1
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4        fix y
     1.5        assume hyp: "Rep_matrix x (fst y) (snd y) \<noteq> 0"
     1.6        show "\<exists> a b. (Rep_matrix x b a \<noteq> 0 & y = (b,a))"
     1.7 -	by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
     1.8 +        by (rule exI[of _ "snd y"], rule exI[of _ "fst y"]) (simp add: hyp)
     1.9      qed
    1.10    then have "finite (?swap`?A)"
    1.11      proof -