src/HOL/Bali/Trans.thy
changeset 62042 6c6ccf573479
parent 56073 29e308b56d23
child 62390 842917225d56
     1.1 --- a/src/HOL/Bali/Trans.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/Bali/Trans.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -236,14 +236,14 @@
     1.4  | InsInitFVar:
     1.5        "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 
     1.6          \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)"
     1.7 ---  {* Notice, that we do not have literal values for @{text vars}. 
     1.8 -The rules for accessing variables (@{text Acc}) and assigning to variables 
     1.9 -(@{text Ass}), test this with the predicate @{text groundVar}.  After 
    1.10 -initialisation is done and the @{text FVar} is evaluated, we can't just 
    1.11 -throw away the @{text InsInitFVar} term and return a literal value, as in the 
    1.12 -cases of @{text New}  or @{text NewC}. Instead we just return the evaluated 
    1.13 -@{text FVar} and test for initialisation in the rule @{text FVar}. 
    1.14 -*}
    1.15 +\<comment>  \<open>Notice, that we do not have literal values for \<open>vars\<close>. 
    1.16 +The rules for accessing variables (\<open>Acc\<close>) and assigning to variables 
    1.17 +(\<open>Ass\<close>), test this with the predicate \<open>groundVar\<close>.  After 
    1.18 +initialisation is done and the \<open>FVar\<close> is evaluated, we can't just 
    1.19 +throw away the \<open>InsInitFVar\<close> term and return a literal value, as in the 
    1.20 +cases of \<open>New\<close>  or \<open>NewC\<close>. Instead we just return the evaluated 
    1.21 +\<open>FVar\<close> and test for initialisation in the rule \<open>FVar\<close>. 
    1.22 +\<close>
    1.23  
    1.24  
    1.25  | AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 
    1.26 @@ -258,7 +258,7 @@
    1.27  
    1.28  (* evaluation of expression lists *)
    1.29  
    1.30 -  -- {* @{text Nil}  is fully evaluated *}
    1.31 +  \<comment> \<open>\<open>Nil\<close>  is fully evaluated\<close>
    1.32  
    1.33  | ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 
    1.34             \<Longrightarrow>
    1.35 @@ -339,8 +339,8 @@
    1.36            \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));;
    1.37                  Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle>
    1.38                 ,Norm (init_class_obj G C s))"
    1.39 --- {* @{text InsInitE} is just used as trick to embed the statement 
    1.40 -@{text "init c"} into an expression*} 
    1.41 +\<comment> \<open>\<open>InsInitE\<close> is just used as trick to embed the statement 
    1.42 +\<open>init c\<close> into an expression\<close> 
    1.43  | InsInitESKIP:
    1.44      "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)"
    1.45