diff -r d09d0f160888 -r 360e3215f029 src/HOL/MicroJava/J/Decl.thy
--- a/src/HOL/MicroJava/J/Decl.thy	Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy	Sun Dec 16 00:18:17 2001 +0100
@@ -4,38 +4,28 @@
     Copyright   1999 Technische Universitaet Muenchen
 *)
 
-header "Class Declarations and whole Programs"
+header "Class Declarations and Programs"
 
 theory Decl = Type:
 
-types	fdecl		(* field declaration, cf. 8.3 (, 9.3) *)
-	= "vname \<times> ty"
+types 
+  fdecl    = "vname \<times> ty"        -- "field declaration, cf. 8.3 (, 9.3)"
+
+  sig      = "mname \<times> ty list"   -- "signature of a method, cf. 8.4.2"
+
+  'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
+
+  'c class = "cname \<times> fdecl list \<times> 'c mdecl list" 
+  -- "class = superclass, fields, methods"
+
+  'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
+
+  'c prog  = "'c cdecl list"     -- "program"
 
 
-types	sig		(* signature of a method, cf. 8.4.2 *)
-	= "mname \<times> ty list"
-
-	'c mdecl		(* method declaration in a class *)
-	= "sig \<times> ty \<times> 'c"
-
-types	'c class		(* class *)
-	= "cname \<times> fdecl list \<times> 'c mdecl list"
-	(* superclass, fields, methods*)
-
-	'c cdecl		(* class declaration, cf. 8.1 *)
-	= "cname \<times> 'c class"
-
-consts
-
-  Object  :: cname	(* name of root class *)
-  ObjectC :: "'c cdecl"	(* decl of root class *)
-
-defs 
-
- ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"
-
-
-types 'c prog = "'c cdecl list"
+constdefs
+  ObjectC :: "'c cdecl" -- "decl of root class"
+  "ObjectC \<equiv> (Object, (arbitrary, [], []))"
 
 
 translations
@@ -46,12 +36,14 @@
   "cdecl c" <= (type) "cname \<times> (c class)"
   "prog  c" <= (type) "(c cdecl) list"
 
-constdefs
 
-  class		:: "'c prog => (cname \<leadsto> 'c class)"
-  "class        \<equiv> map_of"
-  is_class	:: "'c prog => cname => bool"
- "is_class G C  \<equiv> class G C \<noteq> None"
+constdefs
+  class :: "'c prog => (cname \<leadsto> 'c class)"
+  "class \<equiv> map_of"
+
+  is_class :: "'c prog => cname => bool"
+  "is_class G C \<equiv> class G C \<noteq> None"
+
 
 lemma finite_is_class: "finite {C. is_class G C}"
 apply (unfold is_class_def class_def)
@@ -60,11 +52,9 @@
 done
 
 consts
-
-  is_type	:: "'c prog => ty    => bool"
-
+  is_type :: "'c prog => ty    => bool"
 primrec
-"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
+  "is_type G (PrimT pt) = True"
+  "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
 
 end