Corrected implementation of arbitrary on cname.
authorberghofe
Fri Jul 01 14:11:06 2005 +0200 (2005-07-01)
changeset 16644701218c1301c
parent 16643 39cb9fe20fe3
child 16645 a152d6b21c31
Corrected implementation of arbitrary on cname.
src/HOL/MicroJava/JVM/JVMListExample.thy
     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 *}