--- a/src/HOL/Bali/Decl.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/Bali/Decl.thy Tue Jan 03 11:32:55 2006 +0100
@@ -324,7 +324,7 @@
methods:: "mdecl list"
init :: "stmt" --{* initializer *}
-record class = cbody + --{* class *}
+record "class" = cbody + --{* class *}
super :: "qtname" --{* superclass *}
superIfs:: "qtname list" --{* implemented interfaces *}
types
@@ -405,7 +405,7 @@
syntax
iface :: "prog \<Rightarrow> (qtname, iface) table"
- class :: "prog \<Rightarrow> (qtname, class) table"
+ "class" :: "prog \<Rightarrow> (qtname, class) table"
is_iface :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
is_class :: "prog \<Rightarrow> qtname \<Rightarrow> bool"
--- a/src/HOL/Bali/Example.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/Bali/Example.thy Tue Jan 03 11:32:55 2006 +0100
@@ -168,7 +168,7 @@
arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
-BaseCl :: class
+BaseCl :: "class"
"BaseCl \<equiv> \<lparr>access=Public,
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)],
@@ -178,7 +178,7 @@
super=Object,
superIfs=[HasFoo]\<rparr>"
-ExtCl :: class
+ExtCl :: "class"
"ExtCl \<equiv> \<lparr>access=Public,
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)],
methods=[Ext_foo],
@@ -186,7 +186,7 @@
super=Base,
superIfs=[]\<rparr>"
-MainCl :: class
+MainCl :: "class"
"MainCl \<equiv> \<lparr>access=Public,
cfields=[],
methods=[],
--- a/src/HOL/Library/Quotient.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/Library/Quotient.thy Tue Jan 03 11:32:55 2006 +0100
@@ -75,7 +75,7 @@
*}
constdefs
- class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>")
+ "class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>")
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy Tue Jan 03 11:32:55 2006 +0100
@@ -239,7 +239,7 @@
from conforms obtain ST LT rT maxs maxl ins et where
hconf: "G \<turnstile>h hp \<surd>" and
- class: "is_class G C" and
+ "class": "is_class G C" and
meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
phi: "Phi C sig ! pc = Some (ST,LT)" and
frame: "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
@@ -277,7 +277,7 @@
proof (cases "ins!pc")
case (Getfield F C)
with app stk loc phi obtain v vT stk' where
- class: "is_class G C" and
+ "class": "is_class G C" and
field: "field (G, C) F = Some (C, vT)" and
stk: "stk = v # stk'" and
conf: "G,hp \<turnstile> v ::\<preceq> Class C"
@@ -291,7 +291,7 @@
have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
by (auto dest!: non_np_objD)
}
- ultimately show ?thesis using Getfield field class stk hconf wf
+ ultimately show ?thesis using Getfield field "class" stk hconf wf
apply clarsimp
apply (fastsimp intro: wf_prog_ws_prog
dest!: hconfD widen_cfs_fields oconf_objD)
@@ -299,7 +299,7 @@
next
case (Putfield F C)
with app stk loc phi obtain v ref vT stk' where
- class: "is_class G C" and
+ "class": "is_class G C" and
field: "field (G, C) F = Some (C, vT)" and
stk: "stk = v # ref # stk'" and
confv: "G,hp \<turnstile> v ::\<preceq> vT" and
@@ -314,7 +314,7 @@
have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
by (auto dest: non_np_objD)
}
- ultimately show ?thesis using Putfield field class stk confv
+ ultimately show ?thesis using Putfield field "class" stk confv
by clarsimp
next
case (Invoke C mn ps)
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Jan 03 11:32:55 2006 +0100
@@ -325,7 +325,7 @@
obtain ST LT where
hp_ok: "G \<turnstile>h hp \<surd>" and
prehp: "preallocated hp" and
- class: "is_class G C" and
+ "class": "is_class G C" and
phi_pc: "phi C sig ! pc = Some (ST, LT)" and
frame: "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
frames: "correct_frames G hp phi rT sig frs"
@@ -572,7 +572,7 @@
show ?thesis by (rule that)
qed (insert xp', auto) -- "the other instructions don't generate exceptions"
- from state' meth hp_ok class frames phi_pc' frame'
+ from state' meth hp_ok "class" frames phi_pc' frame'
have ?thesis by (unfold correct_state_def) simp
}
ultimately
--- a/src/HOL/MicroJava/J/Decl.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Tue Jan 03 11:32:55 2006 +0100
@@ -15,7 +15,7 @@
'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
- 'c class = "cname \<times> fdecl list \<times> 'c mdecl list"
+ 'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list"
-- "class = superclass, fields, methods"
'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
@@ -33,7 +33,7 @@
constdefs
- class :: "'c prog => (cname \<rightharpoonup> 'c class)"
+ "class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
"class \<equiv> map_of"
is_class :: "'c prog => cname => bool"
--- a/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:16 2006 +0100
+++ b/src/HOL/NanoJava/Decl.thy Tue Jan 03 11:32:55 2006 +0100
@@ -26,7 +26,7 @@
types mdecl
= "mname \<times> methd"
-record class
+record "class"
= super :: cname
flds ::"fdecl list"
methods ::"mdecl list"
@@ -52,7 +52,7 @@
constdefs
- class :: "cname \<rightharpoonup> class"
+ "class" :: "cname \<rightharpoonup> class"
"class \<equiv> map_of Prog"
is_class :: "cname => bool"