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.
cast_ok no longer disabled (thanks to improvement of code generator).
authorberghofe
Thu, 20 Dec 2001 14:59:09 +0100
changeset 12558 f2a87c62b4ae
parent 12557 bb2e4689347e
child 12559 7fb12775ce98
cast_ok no longer disabled (thanks to improvement of code generator).
src/HOL/MicroJava/J/JListExample.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:58:18 2001 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Thu Dec 20 14:59:09 2001 +0100
@@ -66,7 +66,6 @@
 
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}")
-  "cast_ok" ("true????")
 
   "wf" ("true?")
isabelle