author | haftmann |
Tue, 10 Oct 2006 09:17:21 +0200 | |
changeset 20935 | f9a578316eef |
parent 20934 | 2b872c161747 |
child 20936 | dc5dc0e55938 |
--- 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