changeset 12951 | a9fdcb71d252 |
parent 12911 | 704713ca07ea |
child 13091 | 3d12669e599c |
--- a/src/HOL/MicroJava/J/JListExample.thy Tue Feb 26 13:47:19 2002 +0100 +++ b/src/HOL/MicroJava/J/JListExample.thy Tue Feb 26 15:45:32 2002 +0100 @@ -1,11 +1,11 @@ -(* Title: HOL/MicroJava/JVM/JVMListExample.thy +(* Title: HOL/MicroJava/J/JListExample.thy ID: $Id$ Author: Stefan Berghofer *) header {* \isaheader{Example for generating executable code from Java semantics} *} -theory JListExample = Eval: +theory JListExample = Eval + SystemClasses: ML {* Syntax.ambiguity_level := 100000 *}