src/HOL/Bali/Name.thy
changeset 13688 a0b16d42d489
parent 12859 f63315dfffd4
child 14700 2f885b7e5ba7
     1.1 --- a/src/HOL/Bali/Name.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/Name.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -8,11 +8,11 @@
     1.4  theory Name = Basis:
     1.5  
     1.6  (* cf. 6.5 *) 
     1.7 -typedecl tnam		(* ordinary type name, i.e. class or interface name *)
     1.8 -typedecl pname          (* package name *)
     1.9 -typedecl mname		(* method name *)
    1.10 -typedecl vname          (* variable or field name *)
    1.11 -typedecl label          (* label as destination of break or continue *)
    1.12 +typedecl tnam	--{* ordinary type name, i.e. class or interface name *}
    1.13 +typedecl pname  --{* package name *}
    1.14 +typedecl mname  --{* method name *}
    1.15 +typedecl vname  --{* variable or field name *}
    1.16 +typedecl label  --{* label as destination of break or continue *}
    1.17  
    1.18  arities
    1.19    tnam  :: "type"
    1.20 @@ -22,11 +22,11 @@
    1.21    label :: "type"
    1.22  
    1.23  
    1.24 -datatype ename        (* expression name *) 
    1.25 +datatype ename        --{* expression name *} 
    1.26          = VNam vname 
    1.27 -        | Res         (* special name to model the return value of methods *)
    1.28 +        | Res         --{* special name to model the return value of methods *}
    1.29  
    1.30 -datatype lname        (* names for local variables and the This pointer *)
    1.31 +datatype lname        --{* names for local variables and the This pointer *}
    1.32          = EName ename 
    1.33          | This
    1.34  syntax   
    1.35 @@ -37,7 +37,7 @@
    1.36    "VName n" == "EName (VNam n)"
    1.37    "Result"  == "EName Res"
    1.38  
    1.39 -datatype xname		(* names of standard exceptions *)
    1.40 +datatype xname		--{* names of standard exceptions *}
    1.41  	= Throwable
    1.42  	| NullPointer | OutOfMemory | ClassCast   
    1.43  	| NegArrSize  | IndOutBound | ArrStore
    1.44 @@ -50,22 +50,14 @@
    1.45  apply auto
    1.46  done
    1.47  
    1.48 -lemma xn_cases_old:   (* FIXME cf. Example.thy *)
    1.49 -  "ALL xn. xn = Throwable   \<or> xn = NullPointer \<or>  
    1.50 -         xn = OutOfMemory \<or> xn = ClassCast \<or> 
    1.51 -         xn = NegArrSize  \<or> xn = IndOutBound \<or> xn = ArrStore"
    1.52 -apply (rule allI)
    1.53 -apply (induct_tac xn)
    1.54 -apply auto
    1.55 -done
    1.56  
    1.57 -datatype tname	(* type names for standard classes and other type names *)
    1.58 +datatype tname	--{* type names for standard classes and other type names *}
    1.59  	= Object_
    1.60  	| SXcpt_   xname
    1.61  	| TName   tnam
    1.62  
    1.63 -record   qtname = (* qualified tname cf. 6.5.3, 6.5.4*)
    1.64 -          pid :: pname 
    1.65 +record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
    1.66 +          pid :: pname  
    1.67            tid :: tname
    1.68  
    1.69  axclass has_pname < "type"
    1.70 @@ -102,7 +94,7 @@
    1.71    (type) "'a qtname_scheme" <= (type) "\<lparr>pid::pname,tid::tname,\<dots>::'a\<rparr>"
    1.72  
    1.73  
    1.74 -consts java_lang::pname (* package java.lang *)
    1.75 +consts java_lang::pname --{* package java.lang *}
    1.76  
    1.77  consts 
    1.78    Object :: qtname