src/HOL/Bali/Name.thy

 header {* Java names *}
 
 theory Name imports Basis begin
 
 (* cf. 6.5 *) 
-typedecl tnam	--{* ordinary type name, i.e. class or interface name *}
+typedecl tnam   --{* ordinary type name, i.e. class or interface name *}
 typedecl pname  --{* package name *}
 typedecl mname  --{* method name *}
 typedecl vname  --{* variable or field name *}
 typedecl label  --{* label as destination of break or continue *}
 

 
 translations
   "VName n" == "EName (VNam n)"
   "Result"  == "EName Res"
 
-datatype xname		--{* names of standard exceptions *}
-	= Throwable
-	| NullPointer | OutOfMemory | ClassCast   
-	| NegArrSize  | IndOutBound | ArrStore
+datatype xname          --{* names of standard exceptions *}
+        = Throwable
+        | NullPointer | OutOfMemory | ClassCast   
+        | NegArrSize  | IndOutBound | ArrStore
 
 lemma xn_cases: 
   "xn = Throwable   \<or> xn = NullPointer \<or>  
          xn = OutOfMemory \<or> xn = ClassCast \<or> 
          xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
 apply (induct xn)
 apply auto
 done
 
 
-datatype tname	--{* type names for standard classes and other type names *}
-	= Object'
-	| SXcpt'   xname
-	| TName   tnam
+datatype tname  --{* type names for standard classes and other type names *}
+        = Object'
+        | SXcpt'   xname
+        | TName   tnam
 
 record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
           pid :: pname  
           tid :: tname