# HG changeset patch # User haftmann # Date 1136284375 -3600 # Node ID be0705186ff5e7776dfa0eed308dfd6a360c0931 # Parent 59b89f625d687d6b9a14f7fbf38f9850c5e72f1f class now an keyword, quoted where necessary diff -r 59b89f625d68 -r be0705186ff5 src/HOL/Bali/Decl.thy --- 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 \ (qtname, iface) table" - class :: "prog \ (qtname, class) table" + "class" :: "prog \ (qtname, class) table" is_iface :: "prog \ qtname \ bool" is_class :: "prog \ qtname \ bool" diff -r 59b89f625d68 -r be0705186ff5 src/HOL/Bali/Example.thy --- 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 \ qtname \ var" "arr_viewed_from accC C \ {accC,Base,True}StatRef (ClassT C)..arr" -BaseCl :: class +BaseCl :: "class" "BaseCl \ \access=Public, cfields=[(arr, \access=Public,static=True ,type=PrimT Boolean.[]\), (vee, \access=Public,static=False,type=Iface HasFoo \)], @@ -178,7 +178,7 @@ super=Object, superIfs=[HasFoo]\" -ExtCl :: class +ExtCl :: "class" "ExtCl \ \access=Public, cfields=[(vee, \access=Public,static=False,type= PrimT Integer\)], methods=[Ext_foo], @@ -186,7 +186,7 @@ super=Base, superIfs=[]\" -MainCl :: class +MainCl :: "class" "MainCl \ \access=Public, cfields=[], methods=[], diff -r 59b89f625d68 -r be0705186ff5 src/HOL/Library/Quotient.thy --- 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" ("\_\") + "class" :: "'a::equiv => 'a quot" ("\_\") "\a\ == Abs_quot {x. a \ x}" theorem quot_exhaust: "\a. A = \a\" diff -r 59b89f625d68 -r be0705186ff5 src/HOL/MicroJava/BV/BVNoTypeError.thy --- 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 \h hp \" 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 \ v ::\ Class C" @@ -291,7 +291,7 @@ have "\D vs. hp (the_Addr v) = Some (D,vs) \ G \ D \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 \ v ::\ vT" and @@ -314,7 +314,7 @@ have "\D vs. hp (the_Addr ref) = Some (D,vs) \ G \ D \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) diff -r 59b89f625d68 -r be0705186ff5 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy --- 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 \h hp \" 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 diff -r 59b89f625d68 -r be0705186ff5 src/HOL/MicroJava/J/Decl.thy --- 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 \ ty \ 'c" -- "method declaration in a class" - 'c class = "cname \ fdecl list \ 'c mdecl list" + 'c "class" = "cname \ fdecl list \ 'c mdecl list" -- "class = superclass, fields, methods" 'c cdecl = "cname \ 'c class" -- "class declaration, cf. 8.1" @@ -33,7 +33,7 @@ constdefs - class :: "'c prog => (cname \ 'c class)" + "class" :: "'c prog => (cname \ 'c class)" "class \ map_of" is_class :: "'c prog => cname => bool" diff -r 59b89f625d68 -r be0705186ff5 src/HOL/NanoJava/Decl.thy --- 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 \ methd" -record class +record "class" = super :: cname flds ::"fdecl list" methods ::"mdecl list" @@ -52,7 +52,7 @@ constdefs - class :: "cname \ class" + "class" :: "cname \ class" "class \ map_of Prog" is_class :: "cname => bool"