Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
wf is no longer implemented by true (due to change in definition of class_rec).
authorberghofe
Fri, 19 Apr 2002 14:44:50 +0200
changeset 13091 3d12669e599c
parent 13090 4fb7a2f2c1df
child 13092 eae72c47d07f
wf is no longer implemented by true (due to change in definition of class_rec).
src/HOL/MicroJava/J/JListExample.thy file | annotate | diff | comparison | revisions
src/HOL/MicroJava/JVM/JVMListExample.thy file | annotate | diff | comparison | revisions 
--- 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" ("\"\"")
--- 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")
isabelle