--- a/src/HOL/Bali/DeclConcepts.thy Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Thu Mar 12 14:58:32 2015 +0100
@@ -368,7 +368,7 @@
class) to a qualified member declaration: @{text method} *}
definition
- method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
+ "method" :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)"
where "method sig m = (declclass m, mdecl (sig, mthd m))"
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))"
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Thu Mar 12 14:58:32 2015 +0100
@@ -429,14 +429,14 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
assumes s: "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> t"
shows "t \<noteq> TypeError"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
from wt this s show ?thesis by (rule no_type_errors)
qed
@@ -461,12 +461,12 @@
fixes G ("\<Gamma>") and Phi ("\<Phi>")
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
assumes is_class: "is_class \<Gamma> C"
- and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
+ and "method": "method (\<Gamma>,C) (m,[]) = Some (C, b)"
and m: "m \<noteq> init"
defines start: "s \<equiv> start_state \<Gamma> C m"
shows "\<Gamma> \<turnstile> (Normal s) \<midarrow>jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s \<midarrow>jvm\<rightarrow> t"
proof -
- from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
+ from wt is_class "method" have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
unfolding start by (rule BV_correct_initial)
with wt show ?thesis by (rule welltyped_commutes)
qed
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Thu Mar 12 14:58:32 2015 +0100
@@ -811,7 +811,7 @@
\<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
proof -
assume wtprog: "wt_jvm_prog G phi"
- assume method: "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
+ assume "method": "method (G,C) sig = Some (C,rT,maxs,maxl,ins,et)"
assume ins: "ins ! pc = Invoke C' mn pTs"
assume wti: "wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc"
assume state': "Some state' = exec (G, None, hp, (stk,loc,C,sig,pc)#frs)"
@@ -823,7 +823,7 @@
wfprog: "wf_prog wfmb G"
by (simp add: wt_jvm_prog_def)
- from ins method approx
+ from ins "method" approx
obtain s where
heap_ok: "G\<turnstile>h hp\<surd>" and
prealloc:"preallocated hp" and
@@ -880,7 +880,7 @@
from stk' l_o l
have oX_pos: "last (take (Suc (length pTs)) stk) = oX" by simp
- with state' method ins no_xcp oX_conf
+ with state' "method" ins no_xcp oX_conf
obtain ref where oX_Addr: "oX = Addr ref"
by (auto simp add: raise_system_xcpt_def dest: conf_RefTD)
@@ -922,7 +922,7 @@
from loc obj_ty have "fst (the (hp ref)) = D" by (simp add: obj_ty_def)
- with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
+ with oX_Addr oX_pos state' "method" ins stk' l_o l loc obj_ty mD no_xcp
have state'_val:
"state' =
Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined,
@@ -972,7 +972,7 @@
show ?thesis by (simp add: correct_frame_def)
qed
- from state'_val heap_ok mD'' ins method phi_pc s X' l mX
+ from state'_val heap_ok mD'' ins "method" phi_pc s X' l mX
frames s' LT0 c_f is_class_C stk' oX_Addr frame prealloc and l
show ?thesis
apply (simp add: correct_state_def)
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Thu Mar 12 14:58:32 2015 +0100
@@ -177,7 +177,7 @@
qed
consts
- method :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
+ "method" :: "'c prog \<times> cname => ( sig \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)
field :: "'c prog \<times> cname => ( vname \<rightharpoonup> cname \<times> ty )" (* ###curry *)
fields :: "'c prog \<times> cname => ((vname \<times> cname) \<times> ty) list" (* ###curry *)
--- a/src/HOL/NanoJava/TypeRel.thy Tue Mar 10 23:04:40 2015 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Thu Mar 12 14:58:32 2015 +0100
@@ -108,7 +108,7 @@
done
--{* Methods of a class, with inheritance and hiding *}
-definition method :: "cname => (mname \<rightharpoonup> methd)" where
+definition "method" :: "cname => (mname \<rightharpoonup> methd)" where
"method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>