src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 12518 521f2da133be
parent 12442 0ecba8660de7
child 12522 69971d68fe03
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Dec 16 00:18:17 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Dec 16 00:18:44 2001 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4    next_name :: vname
     1.5    "next_name == VName next_nam"
     1.6  
     1.7 -  list_class :: "(nat * nat * bytecode) class"
     1.8 +  list_class :: "jvm_method class"
     1.9    "list_class ==
    1.10      (Object,
    1.11       [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
    1.12 @@ -41,9 +41,9 @@
    1.13          Load 1,
    1.14          Putfield next_name list_name,
    1.15          LitPush Unit,
    1.16 -        Return]))])"
    1.17 +        Return],[]))])"
    1.18  
    1.19 -  test_class :: "(nat * nat * bytecode) class"
    1.20 +  test_class :: "jvm_method class"
    1.21    "test_class ==
    1.22      (Object, [],
    1.23       [((makelist_name, []), PrimT Integer,
    1.24 @@ -70,7 +70,7 @@
    1.25          Load 2,
    1.26          Invoke list_name append_name [RefT (ClassT list_name)],
    1.27          LitPush Unit,
    1.28 -        Return]))])"
    1.29 +        Return],[]))])"
    1.30  
    1.31    example_prg :: jvm_prog
    1.32    "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"