src/HOL/Bali/Name.thy

--- a/src/HOL/Bali/Name.thy	Wed Oct 30 12:44:18 2002 +0100
+++ b/src/HOL/Bali/Name.thy	Thu Oct 31 18:27:10 2002 +0100
@@ -8,11 +8,11 @@
 theory Name = Basis:
 
 (* cf. 6.5 *) 
-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 *)
+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 *}
 
 arities
   tnam  :: "type"
@@ -22,11 +22,11 @@
   label :: "type"
 
 
-datatype ename        (* expression name *) 
+datatype ename        --{* expression name *} 
         = VNam vname 
-        | Res         (* special name to model the return value of methods *)
+        | Res         --{* special name to model the return value of methods *}
 
-datatype lname        (* names for local variables and the This pointer *)
+datatype lname        --{* names for local variables and the This pointer *}
         = EName ename 
         | This
 syntax   
@@ -37,7 +37,7 @@
   "VName n" == "EName (VNam n)"
   "Result"  == "EName Res"
 
-datatype xname		(* names of standard exceptions *)
+datatype xname		--{* names of standard exceptions *}
 	= Throwable
 	| NullPointer | OutOfMemory | ClassCast   
 	| NegArrSize  | IndOutBound | ArrStore
@@ -50,22 +50,14 @@
 apply auto
 done
 
-lemma xn_cases_old:   (* FIXME cf. Example.thy *)
-  "ALL xn. xn = Throwable   \<or> xn = NullPointer \<or>  
-         xn = OutOfMemory \<or> xn = ClassCast \<or> 
-         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
-apply (rule allI)
-apply (induct_tac xn)
-apply auto
-done
 
-datatype tname	(* type names for standard classes and other type names *)
+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 
+record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
+          pid :: pname  
           tid :: tname
 
 axclass has_pname < "type"
@@ -102,7 +94,7 @@
   (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
 
 
-consts java_lang::pname (* package java.lang *)
+consts java_lang::pname --{* package java.lang *}
 
 consts 
   Object :: qtname