changeset 10061 | fe82134773dc |
parent 10042 | 7164dc0d24d8 |
child 11026 | a50365d21144 |
--- a/src/HOL/MicroJava/J/State.thy Fri Sep 22 16:28:04 2000 +0200 +++ b/src/HOL/MicroJava/J/State.thy Fri Sep 22 16:28:53 2000 +0200 @@ -14,7 +14,6 @@ obj = "cname \\<times> fields_" (* class instance with class name and fields *) constdefs - obj_ty :: "obj => ty" "obj_ty obj == Class (fst obj)" @@ -42,9 +41,9 @@ Norm :: "state => xstate" translations - "heap" => "fst" - "locals" => "snd" - "Norm s" == "(None,s)" + "heap" => "fst" + "locals" => "snd" + "Norm s" == "(None,s)" constdefs