# HG changeset patch
# User nipkow
# Date 1380297465 -7200
# Node ID 024fadbd03f02ee4f60d412f56221078debb8cc3
# Parent  ce12e547e6bb9eef5215b69ccf62056580062678# Parent  50673b36232430a52aca8cc7d011cf4b8a9ad0cf
merged

diff -r ce12e547e6bb -r 024fadbd03f0 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:39:34 2013 +0200
+++ b/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:57:45 2013 +0200
@@ -32,6 +32,14 @@
   (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
 by (induction xs arbitrary: i) (auto simp: algebra_simps)
 
+text{* We hide coercion @{const int} applied to @{const length}: *}
+
+abbreviation (output)
+  "isize xs == int (length xs)"
+
+notation isize ("size")
+
+
 subsection "Instructions and Stack Machine"
 
 text_raw{*\snip{instrdef}{0}{1}{% *}