Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/State.thy
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
isabelle