src/HOL/Bali/WellType.thy
changeset 62042 6c6ccf573479
parent 61989 ba8c284d4725
child 62390 842917225d56
     1.1 --- a/src/HOL/Bali/WellType.thy	Sat Jan 02 18:46:36 2016 +0100
     1.2 +++ b/src/HOL/Bali/WellType.thy	Sat Jan 02 18:48:45 2016 +0100
     1.3 @@ -1,13 +1,13 @@
     1.4  (*  Title:      HOL/Bali/WellType.thy
     1.5      Author:     David von Oheimb
     1.6  *)
     1.7 -subsection {* Well-typedness of Java programs *}
     1.8 +subsection \<open>Well-typedness of Java programs\<close>
     1.9  
    1.10  theory WellType
    1.11  imports DeclConcepts
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 +text \<open>
    1.16  improvements over Java Specification 1.0:
    1.17  \begin{itemize}
    1.18  \item methods of Object can be called upon references of interface or array type
    1.19 @@ -26,15 +26,15 @@
    1.20    the dynamic type of objects. Therefore, they can be used for both 
    1.21    checking static types and determining runtime types in transition semantics.
    1.22  \end{itemize}
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26  type_synonym lenv
    1.27 -        = "(lname, ty) table"  --{* local variables, including This and Result*}
    1.28 +        = "(lname, ty) table"  \<comment>\<open>local variables, including This and Result\<close>
    1.29  
    1.30  record env = 
    1.31 -         prg:: "prog"    --{* program *}
    1.32 -         cls:: "qtname"  --{* current package and class name *}
    1.33 -         lcl:: "lenv"    --{* local environment *}     
    1.34 +         prg:: "prog"    \<comment>\<open>program\<close>
    1.35 +         cls:: "qtname"  \<comment>\<open>current package and class name\<close>
    1.36 +         lcl:: "lenv"    \<comment>\<open>local environment\<close>     
    1.37    
    1.38  translations
    1.39    (type) "lenv" <= (type) "(lname, ty) table"
    1.40 @@ -44,7 +44,7 @@
    1.41  
    1.42  
    1.43  abbreviation
    1.44 -  pkg :: "env \<Rightarrow> pname" --{* select the current package from an environment *}
    1.45 +  pkg :: "env \<Rightarrow> pname" \<comment>\<open>select the current package from an environment\<close>
    1.46    where "pkg e == pid (cls e)"
    1.47  
    1.48  subsubsection "Static overloading: maximally specific methods "
    1.49 @@ -52,7 +52,7 @@
    1.50  type_synonym
    1.51    emhead = "ref_ty \<times> mhead"
    1.52  
    1.53 ---{* Some mnemotic selectors for emhead *}
    1.54 +\<comment>\<open>Some mnemotic selectors for emhead\<close>
    1.55  definition
    1.56    "declrefT" :: "emhead \<Rightarrow> ref_ty"
    1.57    where "declrefT = fst"
    1.58 @@ -107,20 +107,20 @@
    1.59  | "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
    1.60  
    1.61  definition
    1.62 -  --{* applicable methods, cf. 15.11.2.1 *}
    1.63 +  \<comment>\<open>applicable methods, cf. 15.11.2.1\<close>
    1.64    appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow>  ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
    1.65    "appl_methds G S rt = (\<lambda> sig. 
    1.66        {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 
    1.67                             G\<turnstile>(parTs sig)[\<preceq>]pTs'})"
    1.68  
    1.69  definition
    1.70 -  --{* more specific methods, cf. 15.11.2.2 *}
    1.71 +  \<comment>\<open>more specific methods, cf. 15.11.2.2\<close>
    1.72    more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where
    1.73    "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')"
    1.74  (*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
    1.75  
    1.76  definition
    1.77 -  --{* maximally specific methods, cf. 15.11.2.2 *}
    1.78 +  \<comment>\<open>maximally specific methods, cf. 15.11.2.2\<close>
    1.79    max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where
    1.80    "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and>
    1.81                            (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
    1.82 @@ -262,13 +262,13 @@
    1.83  | "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2  e\<Colon>Inl T"
    1.84  | "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3  e\<Colon>Inr T"
    1.85  
    1.86 ---{* well-typed statements *}
    1.87 +\<comment>\<open>well-typed statements\<close>
    1.88  
    1.89  | Skip:                                 "E,dt\<Turnstile>Skip\<Colon>\<surd>"
    1.90  
    1.91  | Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
    1.92                                           E,dt\<Turnstile>Expr e\<Colon>\<surd>"
    1.93 -  --{* cf. 14.6 *}
    1.94 +  \<comment>\<open>cf. 14.6\<close>
    1.95  | Lab:  "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>                   
    1.96                                           E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 
    1.97  
    1.98 @@ -276,62 +276,62 @@
    1.99            E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.100                                           E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
   1.101  
   1.102 -  --{* cf. 14.8 *}
   1.103 +  \<comment>\<open>cf. 14.8\<close>
   1.104  | If:   "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.105            E,dt\<Turnstile>c1\<Colon>\<surd>;
   1.106            E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.107                                           E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
   1.108  
   1.109 -  --{* cf. 14.10 *}
   1.110 +  \<comment>\<open>cf. 14.10\<close>
   1.111  | Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
   1.112            E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.113                                           E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
   1.114 -  --{* cf. 14.13, 14.15, 14.16 *}
   1.115 +  \<comment>\<open>cf. 14.13, 14.15, 14.16\<close>
   1.116  | Jmp:                                   "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>"
   1.117  
   1.118 -  --{* cf. 14.16 *}
   1.119 +  \<comment>\<open>cf. 14.16\<close>
   1.120  | Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
   1.121            prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
   1.122                                           E,dt\<Turnstile>Throw e\<Colon>\<surd>"
   1.123 -  --{* cf. 14.18 *}
   1.124 +  \<comment>\<open>cf. 14.18\<close>
   1.125  | Try:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
   1.126            lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
   1.127            \<Longrightarrow>
   1.128                                           E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
   1.129  
   1.130 -  --{* cf. 14.18 *}
   1.131 +  \<comment>\<open>cf. 14.18\<close>
   1.132  | Fin:  "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
   1.133                                           E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
   1.134  
   1.135  | Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
   1.136                                           E,dt\<Turnstile>Init C\<Colon>\<surd>"
   1.137 -  --{* @{term Init} is created on the fly during evaluation (see Eval.thy). 
   1.138 +  \<comment>\<open>@{term Init} is created on the fly during evaluation (see Eval.thy). 
   1.139       The class isn't necessarily accessible from the points @{term Init} 
   1.140       is called. Therefor we only demand @{term is_class} and not 
   1.141       @{term is_acc_class} here. 
   1.142 -   *}
   1.143 +\<close>
   1.144  
   1.145 ---{* well-typed expressions *}
   1.146 +\<comment>\<open>well-typed expressions\<close>
   1.147  
   1.148 -  --{* cf. 15.8 *}
   1.149 +  \<comment>\<open>cf. 15.8\<close>
   1.150  | NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
   1.151                                           E,dt\<Turnstile>NewC C\<Colon>-Class C"
   1.152 -  --{* cf. 15.9 *}
   1.153 +  \<comment>\<open>cf. 15.9\<close>
   1.154  | NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
   1.155            E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.156                                           E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
   1.157  
   1.158 -  --{* cf. 15.15 *}
   1.159 +  \<comment>\<open>cf. 15.15\<close>
   1.160  | Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
   1.161            prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
   1.162                                           E,dt\<Turnstile>Cast T' e\<Colon>-T'"
   1.163  
   1.164 -  --{* cf. 15.19.2 *}
   1.165 +  \<comment>\<open>cf. 15.19.2\<close>
   1.166  | Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
   1.167            prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
   1.168                                           E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
   1.169  
   1.170 -  --{* cf. 15.7.1 *}
   1.171 +  \<comment>\<open>cf. 15.7.1\<close>
   1.172  | Lit:  "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
   1.173                                           E,dt\<Turnstile>Lit x\<Colon>-T"
   1.174  
   1.175 @@ -344,28 +344,28 @@
   1.176             \<Longrightarrow>
   1.177             E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T"
   1.178    
   1.179 -  --{* cf. 15.10.2, 15.11.1 *}
   1.180 +  \<comment>\<open>cf. 15.10.2, 15.11.1\<close>
   1.181  | Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
   1.182            class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
   1.183                                           E,dt\<Turnstile>Super\<Colon>-Class (super c)"
   1.184  
   1.185 -  --{* cf. 15.13.1, 15.10.1, 15.12 *}
   1.186 +  \<comment>\<open>cf. 15.13.1, 15.10.1, 15.12\<close>
   1.187  | Acc:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
   1.188                                           E,dt\<Turnstile>Acc va\<Colon>-T"
   1.189  
   1.190 -  --{* cf. 15.25, 15.25.1 *}
   1.191 +  \<comment>\<open>cf. 15.25, 15.25.1\<close>
   1.192  | Ass:  "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
   1.193            E,dt\<Turnstile>v \<Colon>-T';
   1.194            prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
   1.195                                           E,dt\<Turnstile>va:=v\<Colon>-T'"
   1.196  
   1.197 -  --{* cf. 15.24 *}
   1.198 +  \<comment>\<open>cf. 15.24\<close>
   1.199  | Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
   1.200            E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
   1.201            prg E\<turnstile>T1\<preceq>T2 \<and> T = T2  \<or>  prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
   1.202                                           E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
   1.203  
   1.204 -  --{* cf. 15.11.1, 15.11.2, 15.11.3 *}
   1.205 +  \<comment>\<open>cf. 15.11.1, 15.11.2, 15.11.3\<close>
   1.206  | Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
   1.207            E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
   1.208            max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 
   1.209 @@ -377,7 +377,7 @@
   1.210            methd (prg E) C sig = Some m;
   1.211            E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
   1.212                                           E,dt\<Turnstile>Methd C sig\<Colon>-T"
   1.213 - --{* The class @{term C} is the dynamic class of the method call 
   1.214 + \<comment>\<open>The class @{term C} is the dynamic class of the method call 
   1.215      (cf. Eval.thy). 
   1.216      It hasn't got to be directly accessible from the current package 
   1.217      @{term "(pkg E)"}. 
   1.218 @@ -386,42 +386,42 @@
   1.219      Note that l is just a dummy value. It is only used in the smallstep 
   1.220      semantics. To proof typesafety directly for the smallstep semantics 
   1.221      we would have to assume conformance of l here!
   1.222 -  *}
   1.223 +\<close>
   1.224  
   1.225  | Body: "\<lbrakk>is_class (prg E) D;
   1.226            E,dt\<Turnstile>blk\<Colon>\<surd>;
   1.227            (lcl E) Result = Some T;
   1.228            is_type (prg E) T\<rbrakk> \<Longrightarrow>
   1.229                                           E,dt\<Turnstile>Body D blk\<Colon>-T"
   1.230 ---{* The class @{term D} implementing the method must not directly be 
   1.231 +\<comment>\<open>The class @{term D} implementing the method must not directly be 
   1.232       accessible  from the current package @{term "(pkg E)"}, but can also 
   1.233       be indirectly accessible due to inheritance (enshured in @{term Call})
   1.234      The result type hasn't got to be accessible in Java! (If it is not 
   1.235      accessible you can only assign it to Object).
   1.236      For dummy value l see rule @{term Methd}. 
   1.237 -   *}
   1.238 +\<close>
   1.239  
   1.240 ---{* well-typed variables *}
   1.241 +\<comment>\<open>well-typed variables\<close>
   1.242  
   1.243 -  --{* cf. 15.13.1 *}
   1.244 +  \<comment>\<open>cf. 15.13.1\<close>
   1.245  | LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
   1.246                                           E,dt\<Turnstile>LVar vn\<Colon>=T"
   1.247 -  --{* cf. 15.10.1 *}
   1.248 +  \<comment>\<open>cf. 15.10.1\<close>
   1.249  | FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 
   1.250            accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow>
   1.251                           E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)"
   1.252 -  --{* cf. 15.12 *}
   1.253 +  \<comment>\<open>cf. 15.12\<close>
   1.254  | AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 
   1.255            E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
   1.256                                           E,dt\<Turnstile>e.[i]\<Colon>=T"
   1.257  
   1.258  
   1.259 ---{* well-typed expression lists *}
   1.260 +\<comment>\<open>well-typed expression lists\<close>
   1.261  
   1.262 -  --{* cf. 15.11.??? *}
   1.263 +  \<comment>\<open>cf. 15.11.???\<close>
   1.264  | Nil:                                  "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
   1.265  
   1.266 -  --{* cf. 15.11.??? *}
   1.267 +  \<comment>\<open>cf. 15.11.???\<close>
   1.268  | Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
   1.269            E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
   1.270                                           E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
   1.271 @@ -458,7 +458,7 @@
   1.272  declare not_None_eq [simp del] 
   1.273  declare split_if [split del] split_if_asm [split del]
   1.274  declare split_paired_All [simp del] split_paired_Ex [simp del]
   1.275 -setup {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
   1.276 +setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   1.277  
   1.278  inductive_cases wt_elim_cases [cases set]:
   1.279          "E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T"
   1.280 @@ -494,7 +494,7 @@
   1.281  declare not_None_eq [simp] 
   1.282  declare split_if [split] split_if_asm [split]
   1.283  declare split_paired_All [simp] split_paired_Ex [simp]
   1.284 -setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
   1.285 +setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close>
   1.286  
   1.287  lemma is_acc_class_is_accessible: 
   1.288    "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
   1.289 @@ -522,9 +522,9 @@
   1.290  done
   1.291  
   1.292  
   1.293 -text {* Special versions of some typing rules, better suited to pattern 
   1.294 +text \<open>Special versions of some typing rules, better suited to pattern 
   1.295          match the conclusion (no selectors in the conclusion)
   1.296 -*}
   1.297 +\<close>
   1.298  
   1.299  lemma wt_Call: 
   1.300  "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;  
   1.301 @@ -588,13 +588,13 @@
   1.302  apply auto
   1.303  done
   1.304  
   1.305 ---{* In the special syntax to distinguish the typing judgements for expressions, 
   1.306 +\<comment>\<open>In the special syntax to distinguish the typing judgements for expressions, 
   1.307       statements, variables and expression lists the kind of term corresponds
   1.308       to the kind of type in the end e.g. An statement (injection @{term In3} 
   1.309      into terms, always has type void (injection @{term Inl} into the generalised
   1.310      types. The following simplification procedures establish these kinds of
   1.311      correlation. 
   1.312 - *}
   1.313 +\<close>
   1.314  
   1.315  lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)"
   1.316    by (auto, frule wt_Inj_elim, auto)
   1.317 @@ -608,29 +608,29 @@
   1.318  lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)"
   1.319    by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto)
   1.320  
   1.321 -simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = {*
   1.322 +simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open>
   1.323    fn _ => fn _ => fn ct =>
   1.324      (case Thm.term_of ct of
   1.325        (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   1.326 -    | _ => SOME (mk_meta_eq @{thm wt_expr_eq})) *}
   1.327 +    | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close>
   1.328  
   1.329 -simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = {*
   1.330 +simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open>
   1.331    fn _ => fn _ => fn ct =>
   1.332      (case Thm.term_of ct of
   1.333        (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   1.334 -    | _ => SOME (mk_meta_eq @{thm wt_var_eq})) *}
   1.335 +    | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close>
   1.336  
   1.337 -simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = {*
   1.338 +simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open>
   1.339    fn _ => fn _ => fn ct =>
   1.340      (case Thm.term_of ct of
   1.341        (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   1.342 -    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq})) *}
   1.343 +    | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close>
   1.344  
   1.345 -simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = {*
   1.346 +simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open>
   1.347    fn _ => fn _ => fn ct =>
   1.348      (case Thm.term_of ct of
   1.349        (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE
   1.350 -    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq})) *}
   1.351 +    | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close>
   1.352  
   1.353  lemma wt_elim_BinOp:
   1.354    "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   1.355 @@ -658,14 +658,14 @@
   1.356  apply (simp_all (no_asm_use) split del: split_if_asm)
   1.357  apply (safe del: disjE)
   1.358  (* 17 subgoals *)
   1.359 -apply (tactic {* ALLGOALS (fn i =>
   1.360 +apply (tactic \<open>ALLGOALS (fn i =>
   1.361    if i = 11 then EVERY'
   1.362     [Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [(@{binding E}, NONE, NoSyn)],
   1.363      Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e1\<Colon>-T1" [(@{binding E}, NONE, NoSyn), (@{binding T1}, NONE, NoSyn)],
   1.364      Rule_Insts.thin_tac @{context} "E,dt\<Turnstile>e2\<Colon>-T2" [(@{binding E}, NONE, NoSyn), (@{binding T2}, NONE, NoSyn)]] i
   1.365 -  else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i) *})
   1.366 +  else Rule_Insts.thin_tac @{context} "All P" [(@{binding P}, NONE, NoSyn)] i)\<close>)
   1.367  (*apply (safe del: disjE elim!: wt_elim_cases)*)
   1.368 -apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*})
   1.369 +apply (tactic \<open>ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})\<close>)
   1.370  apply (simp_all (no_asm_use) split del: split_if_asm)
   1.371  apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *)
   1.372  apply (blast del: equalityCE dest: sym [THEN trans])+