# HG changeset patch
# User berghofe
# Date 1019220290 -7200
# Node ID 3d12669e599c33cf225fd9ab7ab41578b571ce02
# Parent  4fb7a2f2c1df1b53432930588d1a2f2d4432b13a
wf is no longer implemented by true (due to change in definition of class_rec).

diff -r 4fb7a2f2c1df -r 3d12669e599c src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Fri Apr 19 14:43:16 2002 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Fri Apr 19 14:44:50 2002 +0200
@@ -67,8 +67,6 @@
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
 
-  "wf" ("true?")
-
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
   "arbitrary" :: "cname" ("\"\"")
diff -r 4fb7a2f2c1df -r 3d12669e599c src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Apr 19 14:43:16 2002 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Fri Apr 19 14:44:50 2002 +0200
@@ -96,8 +96,6 @@
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
 
-  "wf" ("true?")
-
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
   "arbitrary" :: "cname" ("Object")