src/HOL/Bali/Evaln.thy
changeset 58887 38db8ddc0f57
parent 58251 b13e5c3497f5
child 58963 26bf09b95dda
     1.1 --- a/src/HOL/Bali/Evaln.thy	Sun Nov 02 17:58:35 2014 +0100
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Sun Nov 02 18:16:19 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Bali/Evaln.thy
     1.5      Author:     David von Oheimb and Norbert Schirmer
     1.6  *)
     1.7 -header {* Operational evaluation (big-step) semantics of Java expressions and 
     1.8 +subsection {* Operational evaluation (big-step) semantics of Java expressions and 
     1.9            statements
    1.10  *}
    1.11  
    1.12 @@ -401,7 +401,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -section {* evaln implies eval *}
    1.17 +subsubsection {* evaln implies eval *}
    1.18  
    1.19  lemma evaln_eval:  
    1.20    assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
    1.21 @@ -510,7 +510,7 @@
    1.22  
    1.23  declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
    1.24  
    1.25 -section {* eval implies evaln *}
    1.26 +subsubsection {* eval implies evaln *}
    1.27  lemma eval_evaln: 
    1.28    assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
    1.29    shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"