src/HOL/NanoJava/TypeRel.thy
changeset 11565 ab004c0ecc63
parent 11558 6539627881e8
child 11626 0dbfb578bf75
     1.1 --- a/src/HOL/NanoJava/TypeRel.thy	Mon Sep 17 19:49:09 2001 +0200
     1.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Fri Sep 21 18:23:15 2001 +0200
     1.3 @@ -31,13 +31,13 @@
     1.4    field  :: "cname => (fname \<leadsto> ty)"
     1.5  
     1.6  
     1.7 -text {* The rest of this theory is not actually used. *}
     1.8 +subsection "Declarations and properties not used in the meta theory"
     1.9  
    1.10 -text{* direct subclass relation *}
    1.11 +text{* Direct subclass relation *}
    1.12  defs
    1.13   subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
    1.14  
    1.15 -text{* widening, viz. method invocation conversion *}
    1.16 +text{* Widening, viz. method invocation conversion *}
    1.17  inductive widen intros 
    1.18    refl   [intro!, simp]:           "T \<preceq> T"
    1.19    subcls         : "C\<preceq>C D \<Longrightarrow> Class C \<preceq> Class D"
    1.20 @@ -121,7 +121,7 @@
    1.21  apply simp
    1.22  done
    1.23  
    1.24 ---{* methods of a class, with inheritance and hiding *}
    1.25 +--{* Methods of a class, with inheritance and hiding *}
    1.26  defs method_def: "method C \<equiv> class_rec C methods"
    1.27  
    1.28  lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
    1.29 @@ -132,7 +132,7 @@
    1.30  done
    1.31  
    1.32  
    1.33 ---{* fields of a class, with inheritance and hiding *}
    1.34 +--{* Fields of a class, with inheritance and hiding *}
    1.35  defs field_def: "field C \<equiv> class_rec C fields"
    1.36  
    1.37  lemma fields_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>