# 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}{% *}