src/HOL/Bali/Name.thy
changeset 17160 fb65eda72fc7
parent 16417 9bc16273c2d4
child 19726 df95778b4c2f
     1.1 --- a/src/HOL/Bali/Name.thy	Sun Aug 28 16:04:43 2005 +0200
     1.2 +++ b/src/HOL/Bali/Name.thy	Sun Aug 28 16:04:44 2005 +0200
     1.3 @@ -13,14 +13,6 @@
     1.4  typedecl vname  --{* variable or field name *}
     1.5  typedecl label  --{* label as destination of break or continue *}
     1.6  
     1.7 -arities
     1.8 -  tnam  :: "type"
     1.9 -  pname :: "type"
    1.10 -  vname :: "type"
    1.11 -  mname :: "type"
    1.12 -  label :: "type"
    1.13 -
    1.14 -
    1.15  datatype ename        --{* expression name *} 
    1.16          = VNam vname 
    1.17          | Res         --{* special name to model the return value of methods *}
    1.18 @@ -75,11 +67,10 @@
    1.19  defs (overloaded)
    1.20  tname_tname_def: "tname (t::tname) \<equiv> t"
    1.21  
    1.22 -axclass has_qtname < "type"
    1.23 +axclass has_qtname < type
    1.24  consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    1.25  
    1.26 -(* Declare qtname as instance of has_qtname *)
    1.27 -instance qtname_ext_type::("type") has_qtname ..
    1.28 +instance qtname_ext_type :: (type) has_qtname ..
    1.29  
    1.30  defs (overloaded)
    1.31  qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
    1.32 @@ -108,4 +99,3 @@
    1.33  lemma SXcpt_inject [simp]: "(SXcpt xn = SXcpt xm) = (xn = xm)"
    1.34  by (simp add: SXcpt_def)
    1.35  end
    1.36 -