simplified a proof
authorpaulson
Mon Feb 14 10:24:58 2005 +0100 (2005-02-14)
changeset 155329712d41db5b8
parent 15531 08c8dad8e399
child 15533 accd51fdae3c
simplified a proof
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Sun Feb 13 17:15:14 2005 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 14 10:24:58 2005 +0100
     1.3 @@ -548,8 +548,7 @@
     1.4    case (Suc m)
     1.5    have nSuc: "n = Suc m" . 
     1.6    have mlessn: "m<n" by (simp add: nSuc)
     1.7 -  have "a \<in> h ` {i. i < n}" using aA by blast
     1.8 -  then obtain k where hkeq: "h k = a" and klessn: "k<n" by blast
     1.9 +  from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
    1.10    let ?hm = "swap k m h"
    1.11    have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
    1.12      by (simp add: inj_on_swap_iff inj_on)