src/HOL/MicroJava/J/TypeRel.thy
changeset 53374 a14d2a854c02
parent 45970 b6d0cff57d96
child 55017 2df6ad1dbd66
     1.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -144,8 +144,8 @@
     1.4        where "class": "class G C = Some (D', fs', ms')"
     1.5        unfolding class_def by(auto dest!: weak_map_of_SomeI)
     1.6      hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
     1.7 -    hence "(C, D') \<in> (subcls1 G)^+" ..
     1.8 -    also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
     1.9 +    hence *: "(C, D') \<in> (subcls1 G)^+" ..
    1.10 +    also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
    1.11      with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
    1.12      finally show False using acyc by(auto simp add: acyclic_def)
    1.13    qed