src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 16644 701218c1301c
parent 16417 9bc16273c2d4
child 16770 1f1b1fae30e4
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Jul 01 14:10:02 2005 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Jul 01 14:11:06 2005 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  
     1.5    "arbitrary" ("(raise ERROR)")
     1.6    "arbitrary" :: "val" ("{* Unit *}")
     1.7 -  "arbitrary" :: "cname" ("Object")
     1.8 +  "arbitrary" :: "cname" ("{* Object *}")
     1.9  
    1.10    "list_nam" ("\"list\"")
    1.11    "test_nam" ("\"test\"")
    1.12 @@ -115,7 +115,7 @@
    1.13  
    1.14  subsection {* Single step execution *}
    1.15  
    1.16 -generate_code 
    1.17 +generate_code
    1.18    test = "exec (E, start_state E test_name makelist_name)"
    1.19  
    1.20  ML {* test *}