changeset 11372 | 648795477bb5 |
parent 11070 | cc421547e744 |
child 12517 | 360e3215f029 |
--- a/src/HOL/MicroJava/J/State.thy Mon Jun 11 19:21:13 2001 +0200 +++ b/src/HOL/MicroJava/J/State.thy Tue Jun 12 14:11:00 2001 +0200 @@ -25,7 +25,7 @@ | ClassCast | OutOfMemory -types aheap = "loc \<leadsto> obj" (* "heap" used in a translation below *) +types aheap = "loc \<leadsto> obj" (** "heap" used in a translation below **) locals = "vname \<leadsto> val" state (* simple state, i.e. variable contents *)