author | kleing |
Mon, 01 Aug 2011 20:21:11 +0200 | |
changeset 44881 | 823549d46960 |
parent 44880 | 9be0f4a6f155 |
child 44882 | f67c93f52d13 |
1.1 --- a/src/HOL/IMP/Comp_Rev.thy Mon Aug 01 19:53:30 2011 +0200 1.2 +++ b/src/HOL/IMP/Comp_Rev.thy Mon Aug 01 20:21:11 2011 +0200 1.3 @@ -188,7 +188,7 @@ 1.4 "1 \<le> isize (acomp a)" 1.5 by (induct a) auto 1.6 1.7 -lemma exits_acomp [simp]: 1.8 +lemma acomp_exits [simp]: 1.9 "exits (acomp a) = {isize (acomp a)}" 1.10 by (auto simp: exits_def acomp_size) 1.11