src/HOL/MicroJava/J/JListExample.thy
changeset 32356 e11cd88e6ade
parent 28524 644b62cf678f
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Mon Aug 10 13:34:50 2009 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Aug 11 10:05:16 2009 +0200
     1.3 @@ -1,12 +1,11 @@
     1.4  (*  Title:      HOL/MicroJava/J/JListExample.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Stefan Berghofer
     1.7  *)
     1.8  
     1.9  header {* \isaheader{Example for generating executable code from Java semantics} *}
    1.10  
    1.11  theory JListExample
    1.12 -imports Eval SystemClasses
    1.13 +imports Eval
    1.14  begin
    1.15  
    1.16  ML {* Syntax.ambiguity_level := 100000 *}