1.1 --- a/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:20:02 2013 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Fri Sep 27 17:57:30 2013 +0200
     1.3 @@ -32,6 +32,14 @@
     1.4    (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
     1.5  by (induction xs arbitrary: i) (auto simp: algebra_simps)
     1.6  
     1.7 +text{* We hide coercion @{const int} applied to @{const length}: *}
     1.8 +
     1.9 +abbreviation (output)
    1.10 +  "isize xs == int (length xs)"
    1.11 +
    1.12 +notation isize ("size")
    1.13 +
    1.14 +
    1.15  subsection "Instructions and Stack Machine"
    1.16  
    1.17  text_raw{*\snip{instrdef}{0}{1}{% *}