src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 13101 90b31354fe15
parent 13091 3d12669e599c
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 12:15:48 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Apr 30 13:00:29 2002 +0200
     1.3 @@ -72,10 +72,10 @@
     1.4          Load 0,
     1.5          Load 1,
     1.6          Invoke list_name append_name [Class list_name],
     1.7 +        Pop,
     1.8          Load 0,
     1.9          Load 2,
    1.10          Invoke list_name append_name [Class list_name],
    1.11 -        LitPush Unit,
    1.12          Return]"
    1.13  
    1.14    test_class :: "jvm_method class"