src/HOL/Bali/DeclConcepts.thy
changeset 58887 38db8ddc0f57
parent 55518 1ddb2edf5ceb
child 59682 d662d096f72b
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sun Nov 02 17:58:35 2014 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sun Nov 02 18:16:19 2014 +0100
     1.3 @@ -1,12 +1,12 @@
     1.4  (*  Title:      HOL/Bali/DeclConcepts.thy
     1.5      Author:     Norbert Schirmer
     1.6  *)
     1.7 -header {* Advanced concepts on Java declarations like overriding, inheritance,
     1.8 +subsection {* Advanced concepts on Java declarations like overriding, inheritance,
     1.9  dynamic method lookup*}
    1.10  
    1.11  theory DeclConcepts imports TypeRel begin
    1.12  
    1.13 -section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
    1.14 +subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
    1.15  
    1.16  definition is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" where
    1.17  "is_public G qn = (case class G qn of
    1.18 @@ -1389,7 +1389,7 @@
    1.19    qed
    1.20  qed
    1.21  
    1.22 -section "fields and methods"
    1.23 +subsubsection "fields and methods"
    1.24  
    1.25  
    1.26  type_synonym
    1.27 @@ -2282,7 +2282,7 @@
    1.28  apply assumption
    1.29  done
    1.30  
    1.31 -section "calculation of the superclasses of a class"
    1.32 +subsubsection "calculation of the superclasses of a class"
    1.33  
    1.34  definition
    1.35    superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where