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 and match_exception_entry no longer disabled (thanks to
authorberghofe
Thu, 20 Dec 2001 15:00:02 +0100
changeset 12559 7fb12775ce98
parent 12558 f2a87c62b4ae
child 12560 5820841f21fd
cast_ok and match_exception_entry no longer disabled (thanks to improvement of code generator).
src/HOL/MicroJava/JVM/JVMListExample.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 14:59:09 2001 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Thu Dec 20 15:00:02 2001 +0100
@@ -87,8 +87,6 @@
 
 consts_code
   "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
-  "cast_ok" ("true????")
-  "match_exception_entry" ("true????")
 
   "wf" ("true?")
isabelle