changeset 30235 | 58d147683393 |
parent 24783 | 5a3e336a2e37 |
child 32356 | e11cd88e6ade |
--- a/src/HOL/MicroJava/J/State.thy Tue Mar 03 17:05:18 2009 +0100 +++ b/src/HOL/MicroJava/J/State.thy Wed Mar 04 10:47:20 2009 +0100 @@ -41,7 +41,7 @@ "Norm s" == "(None,s)" "abrupt" => "fst" "store" => "snd" - "lookup_obj s a'" == "the (heap s (the_Addr a'))" + "lookup_obj s a'" == "CONST the (heap s (the_Addr a'))" constdefs