src/HOL/NanoJava/Decl.thy

 (*  Title:      HOL/NanoJava/Decl.thy
-    ID:         $Id$
     Author:     David von Oheimb
     Copyright   2001 Technische Universitaet Muenchen
 *)
 
 header "Types, class Declarations, and whole programs"

 datatype ty
   = NT           --{* null type  *}
   | Class cname  --{* class type *}
 
 text{* Field declaration *}
-types	fdecl		
-	= "fname \<times> ty"
+types   fdecl           
+        = "fname \<times> ty"
 
-record  methd		
-	= par :: ty 
+record  methd           
+        = par :: ty 
           res :: ty 
           lcl ::"(vname \<times> ty) list"
           bdy :: stmt
 
 text{* Method declaration *}
-types	mdecl
+types   mdecl
         = "mname \<times> methd"
 
-record	"class"
-	= super   :: cname
+record  "class"
+        = super   :: cname
           flds    ::"fdecl list"
           methods ::"mdecl list"
 
 text{* Class declaration *}
-types	cdecl
-	= "cname \<times> class"
+types   cdecl
+        = "cname \<times> class"
 
 types   prog
         = "cdecl list"
 
 translations

   "cdecl" \<leftharpoondown> (type)"cname \<times> class"
   "prog " \<leftharpoondown> (type)"cdecl list"
 
 consts
 
-  Prog    :: prog	--{* program as a global value *}
-  Object  :: cname	--{* name of root class *}
+  Prog    :: prog       --{* program as a global value *}
+  Object  :: cname      --{* name of root class *}
 
 
 constdefs
-  "class"	     :: "cname \<rightharpoonup> class"
+ "class"     :: "cname \<rightharpoonup> class"
  "class      \<equiv> map_of Prog"
 
   is_class   :: "cname => bool"
  "is_class C \<equiv> class C \<noteq> None"