src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 13091 3d12669e599c
parent 13052 3bf41c474a88
child 13101 90b31354fe15
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Apr 19 14:43:16 2002 +0200
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Apr 19 14:44:50 2002 +0200
     1.3 @@ -96,8 +96,6 @@
     1.4  consts_code
     1.5    "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
     1.6  
     1.7 -  "wf" ("true?")
     1.8 -
     1.9    "arbitrary" ("(raise ERROR)")
    1.10    "arbitrary" :: "val" ("{* Unit *}")
    1.11    "arbitrary" :: "cname" ("Object")