# HG changeset patch
# User kleing
# Date 1312222871 -7200
# Node ID 823549d46960183377c5a3884c6bbe3c8a828902
# Parent  9be0f4a6f155018e762d26f7279a97055f1d84b6
more consistent naming in IMP/Comp_Rev

diff -r 9be0f4a6f155 -r 823549d46960 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Mon Aug 01 19:53:30 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Mon Aug 01 20:21:11 2011 +0200
@@ -188,7 +188,7 @@
   "1 \<le> isize (acomp a)"
   by (induct a) auto
 
-lemma exits_acomp [simp]:
+lemma acomp_exits [simp]:
   "exits (acomp a) = {isize (acomp a)}"
   by (auto simp: exits_def acomp_size)