src/HOL/Bali/Example.thy
changeset 62042 6c6ccf573479
parent 61424 c3658c18b7bc
child 62145 5b946c81dfbf
     1.1 --- a/src/HOL/Bali/Example.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -1,13 +1,13 @@
     1.4  (*  Title:      HOL/Bali/Example.thy
     1.5      Author:     David von Oheimb
     1.6  *)
     1.7 -subsection {* Example Bali program *}
     1.8 +subsection \<open>Example Bali program\<close>
     1.9  
    1.10  theory Example
    1.11  imports Eval WellForm
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16  The following example Bali program includes:
    1.17  \begin{itemize}
    1.18  \item class and interface declarations with inheritance, hiding of fields,
    1.19 @@ -52,7 +52,7 @@
    1.20    }
    1.21  }
    1.22  \end{verbatim}
    1.23 -*}
    1.24 +\<close>
    1.25  declare widen.null [intro]
    1.26  
    1.27  lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.28 @@ -894,7 +894,7 @@
    1.29  
    1.30  declare member_is_static_simp [simp]
    1.31  declare wt.Skip [rule del] wt.Init [rule del]
    1.32 -ML {* ML_Thms.bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros}) *}
    1.33 +ML \<open>ML_Thms.bind_thms ("wt_intros", map (rewrite_rule @{context} @{thms id_def}) @{thms wt.intros})\<close>
    1.34  lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    1.35  lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    1.36  
    1.37 @@ -1187,9 +1187,9 @@
    1.38  declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
    1.39          Base_foo_defs  [simp]
    1.40  
    1.41 -ML {* ML_Thms.bind_thms ("eval_intros", map 
    1.42 +ML \<open>ML_Thms.bind_thms ("eval_intros", map 
    1.43          (simplify (@{context} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o 
    1.44 -         rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
    1.45 +         rewrite_rule @{context} [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros})\<close>
    1.46  lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
    1.47  
    1.48  axiomatization