Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more consistent naming in IMP/Comp_Rev
authorkleing
Mon, 01 Aug 2011 20:21:11 +0200
changeset 44010 823549d46960
parent 44009 9be0f4a6f155
child 44011 f67c93f52d13
more consistent naming in IMP/Comp_Rev
src/HOL/IMP/Comp_Rev.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle