class now an keyword, quoted where necessary
authorhaftmann
Tue Jan 03 11:32:55 2006 +0100 (2006-01-03)
changeset 18551be0705186ff5
parent 18550 59b89f625d68
child 18552 30911da9fb27
class now an keyword, quoted where necessary
src/HOL/Bali/Decl.thy
src/HOL/Bali/Example.thy
src/HOL/Library/Quotient.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/NanoJava/Decl.thy
     1.1 --- a/src/HOL/Bali/Decl.thy	Tue Jan 03 11:32:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/Decl.thy	Tue Jan 03 11:32:55 2006 +0100
     1.3 @@ -324,7 +324,7 @@
     1.4           methods:: "mdecl list"
     1.5           init   :: "stmt"       --{* initializer *}
     1.6  
     1.7 -record class = cbody +           --{* class *}
     1.8 +record "class" = cbody +           --{* class *}
     1.9          super   :: "qtname"      --{* superclass *}
    1.10          superIfs:: "qtname list" --{* implemented interfaces *}
    1.11  types	
    1.12 @@ -405,7 +405,7 @@
    1.13  
    1.14  syntax
    1.15    iface     :: "prog  \<Rightarrow> (qtname, iface) table"
    1.16 -  class     :: "prog  \<Rightarrow> (qtname, class) table"
    1.17 +  "class"     :: "prog  \<Rightarrow> (qtname, class) table"
    1.18    is_iface  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    1.19    is_class  :: "prog  \<Rightarrow> qtname  \<Rightarrow> bool"
    1.20  
     2.1 --- a/src/HOL/Bali/Example.thy	Tue Jan 03 11:32:16 2006 +0100
     2.2 +++ b/src/HOL/Bali/Example.thy	Tue Jan 03 11:32:55 2006 +0100
     2.3 @@ -168,7 +168,7 @@
     2.4  arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
     2.5  "arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
     2.6  
     2.7 -BaseCl :: class
     2.8 +BaseCl :: "class"
     2.9  "BaseCl \<equiv> \<lparr>access=Public,
    2.10             cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
    2.11  	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
    2.12 @@ -178,7 +178,7 @@
    2.13             super=Object,
    2.14             superIfs=[HasFoo]\<rparr>"
    2.15    
    2.16 -ExtCl  :: class
    2.17 +ExtCl  :: "class"
    2.18  "ExtCl  \<equiv> \<lparr>access=Public,
    2.19             cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
    2.20             methods=[Ext_foo],
    2.21 @@ -186,7 +186,7 @@
    2.22             super=Base,
    2.23             superIfs=[]\<rparr>"
    2.24  
    2.25 -MainCl :: class
    2.26 +MainCl :: "class"
    2.27  "MainCl \<equiv> \<lparr>access=Public,
    2.28             cfields=[], 
    2.29             methods=[], 
     3.1 --- a/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:16 2006 +0100
     3.2 +++ b/src/HOL/Library/Quotient.thy	Tue Jan 03 11:32:55 2006 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4  *}
     3.5  
     3.6  constdefs
     3.7 -  class :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     3.8 +  "class" :: "'a::equiv => 'a quot"    ("\<lfloor>_\<rfloor>")
     3.9    "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"
    3.10  
    3.11  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
     4.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Jan 03 11:32:16 2006 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Tue Jan 03 11:32:55 2006 +0100
     4.3 @@ -239,7 +239,7 @@
     4.4  
     4.5      from conforms obtain  ST LT rT maxs maxl ins et where
     4.6        hconf:  "G \<turnstile>h hp \<surd>" and
     4.7 -      class:  "is_class G C" and
     4.8 +      "class":  "is_class G C" and
     4.9        meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
    4.10        phi:    "Phi C sig ! pc = Some (ST,LT)" and
    4.11        frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
    4.12 @@ -277,7 +277,7 @@
    4.13      proof (cases "ins!pc")
    4.14        case (Getfield F C) 
    4.15        with app stk loc phi obtain v vT stk' where
    4.16 -        class: "is_class G C" and
    4.17 +        "class": "is_class G C" and
    4.18          field: "field (G, C) F = Some (C, vT)" and
    4.19          stk:   "stk = v # stk'" and
    4.20          conf:  "G,hp \<turnstile> v ::\<preceq> Class C"
    4.21 @@ -291,7 +291,7 @@
    4.22          have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C" 
    4.23            by (auto dest!: non_np_objD)
    4.24        }
    4.25 -      ultimately show ?thesis using Getfield field class stk hconf wf
    4.26 +      ultimately show ?thesis using Getfield field "class" stk hconf wf
    4.27          apply clarsimp
    4.28          apply (fastsimp intro: wf_prog_ws_prog
    4.29  	  dest!: hconfD widen_cfs_fields oconf_objD)
    4.30 @@ -299,7 +299,7 @@
    4.31      next
    4.32        case (Putfield F C)
    4.33        with app stk loc phi obtain v ref vT stk' where
    4.34 -        class: "is_class G C" and
    4.35 +        "class": "is_class G C" and
    4.36          field: "field (G, C) F = Some (C, vT)" and
    4.37          stk:   "stk = v # ref # stk'" and
    4.38          confv: "G,hp \<turnstile> v ::\<preceq> vT" and
    4.39 @@ -314,7 +314,7 @@
    4.40          have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
    4.41            by (auto dest: non_np_objD)
    4.42        }
    4.43 -      ultimately show ?thesis using Putfield field class stk confv
    4.44 +      ultimately show ?thesis using Putfield field "class" stk confv
    4.45          by clarsimp
    4.46      next      
    4.47        case (Invoke C mn ps)
     5.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 03 11:32:16 2006 +0100
     5.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Jan 03 11:32:55 2006 +0100
     5.3 @@ -325,7 +325,7 @@
     5.4      obtain ST LT where
     5.5        hp_ok:  "G \<turnstile>h hp \<surd>" and
     5.6        prehp:  "preallocated hp" and
     5.7 -      class:  "is_class G C" and
     5.8 +      "class":  "is_class G C" and
     5.9        phi_pc: "phi C sig ! pc = Some (ST, LT)" and
    5.10        frame:  "correct_frame G hp (ST, LT) maxl ins (stk, loc, C, sig, pc)" and
    5.11        frames: "correct_frames G hp phi rT sig frs"
    5.12 @@ -572,7 +572,7 @@
    5.13        show ?thesis by (rule that)
    5.14      qed (insert xp', auto) -- "the other instructions don't generate exceptions"
    5.15  
    5.16 -    from state' meth hp_ok class frames phi_pc' frame' 
    5.17 +    from state' meth hp_ok "class" frames phi_pc' frame' 
    5.18      have ?thesis by (unfold correct_state_def) simp
    5.19    }
    5.20    ultimately
     6.1 --- a/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:16 2006 +0100
     6.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Tue Jan 03 11:32:55 2006 +0100
     6.3 @@ -15,7 +15,7 @@
     6.4  
     6.5    'c mdecl = "sig \<times> ty \<times> 'c"     -- "method declaration in a class"
     6.6  
     6.7 -  'c class = "cname \<times> fdecl list \<times> 'c mdecl list" 
     6.8 +  'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" 
     6.9    -- "class = superclass, fields, methods"
    6.10  
    6.11    'c cdecl = "cname \<times> 'c class"  -- "class declaration, cf. 8.1"
    6.12 @@ -33,7 +33,7 @@
    6.13  
    6.14  
    6.15  constdefs
    6.16 -  class :: "'c prog => (cname \<rightharpoonup> 'c class)"
    6.17 +  "class" :: "'c prog => (cname \<rightharpoonup> 'c class)"
    6.18    "class \<equiv> map_of"
    6.19  
    6.20    is_class :: "'c prog => cname => bool"
     7.1 --- a/src/HOL/NanoJava/Decl.thy	Tue Jan 03 11:32:16 2006 +0100
     7.2 +++ b/src/HOL/NanoJava/Decl.thy	Tue Jan 03 11:32:55 2006 +0100
     7.3 @@ -26,7 +26,7 @@
     7.4  types	mdecl
     7.5          = "mname \<times> methd"
     7.6  
     7.7 -record	class
     7.8 +record	"class"
     7.9  	= super   :: cname
    7.10            flds    ::"fdecl list"
    7.11            methods ::"mdecl list"
    7.12 @@ -52,7 +52,7 @@
    7.13  
    7.14  
    7.15  constdefs
    7.16 -  class	     :: "cname \<rightharpoonup> class"
    7.17 +  "class"	     :: "cname \<rightharpoonup> class"
    7.18   "class      \<equiv> map_of Prog"
    7.19  
    7.20    is_class   :: "cname => bool"