| changeset 21113 | 5b76e541cc0a |
| parent 20935 | f9a578316eef |
| child 22271 | 51a80e238b29 |
--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 31 09:28:55 2006 +0100 +++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 31 09:28:56 2006 +0100 @@ -449,7 +449,7 @@ "some_elem" ("hd") code_const some_elem - (SML target_atom "hd") + (SML "hd") lemma JVM_sup_unfold [code]: "JVMType.sup S m n = lift2 (Opt.sup