src/HOL/Bali/WellForm.thy
changeset 58887 38db8ddc0f57
parent 55518 1ddb2edf5ceb
child 59897 d1e7f56bcd79
     1.1 --- a/src/HOL/Bali/WellForm.thy	Sun Nov 02 17:58:35 2014 +0100
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Sun Nov 02 18:16:19 2014 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     David von Oheimb and Norbert Schirmer
     1.5  *)
     1.6  
     1.7 -header {* Well-formedness of Java programs *}
     1.8 +subsection {* Well-formedness of Java programs *}
     1.9  theory WellForm imports DefiniteAssignment begin
    1.10  
    1.11  text {*
    1.12 @@ -27,7 +27,7 @@
    1.13  \end{itemize}
    1.14  *}
    1.15  
    1.16 -section "well-formed field declarations"
    1.17 +subsubsection "well-formed field declarations"
    1.18  text  {* well-formed field declaration (common part for classes and interfaces),
    1.19          cf. 8.3 and (9.3) *}
    1.20  
    1.21 @@ -42,7 +42,7 @@
    1.22  
    1.23  
    1.24  
    1.25 -section "well-formed method declarations"
    1.26 +subsubsection "well-formed method declarations"
    1.27    (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
    1.28    (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
    1.29  
    1.30 @@ -202,7 +202,7 @@
    1.31  apply auto
    1.32  done
    1.33  
    1.34 -section "well-formed interface declarations"
    1.35 +subsubsection "well-formed interface declarations"
    1.36    (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
    1.37  
    1.38  text {*
    1.39 @@ -273,7 +273,7 @@
    1.40  apply auto
    1.41  done
    1.42  
    1.43 -section "well-formed class declarations"
    1.44 +subsubsection "well-formed class declarations"
    1.45    (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
    1.46     class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
    1.47  
    1.48 @@ -500,7 +500,7 @@
    1.49  done
    1.50  
    1.51  
    1.52 -section "well-formed programs"
    1.53 +subsubsection "well-formed programs"
    1.54    (* well-formed program, cf. 8.1, 9.1 *)
    1.55  
    1.56  text {*