changeset 20935 | f9a578316eef |
parent 20593 | 5af400cc64d5 |
child 21113 | 5b76e541cc0a |
--- a/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 10 09:17:20 2006 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Tue Oct 10 09:17:21 2006 +0200 @@ -449,7 +449,7 @@ "some_elem" ("hd") code_const some_elem - (SML "{*hd*}") + (SML target_atom "hd") lemma JVM_sup_unfold [code]: "JVMType.sup S m n = lift2 (Opt.sup