src/HOL/Bali/Name.thy
changeset 12859 f63315dfffd4
parent 12858 6214f03d6d27
child 13688 a0b16d42d489
     1.1 --- a/src/HOL/Bali/Name.thy	Mon Jan 28 18:51:48 2002 +0100
     1.2 +++ b/src/HOL/Bali/Name.thy	Mon Jan 28 23:35:20 2002 +0100
     1.3 @@ -71,8 +71,7 @@
     1.4  axclass has_pname < "type"
     1.5  consts pname::"'a::has_pname \<Rightarrow> pname"
     1.6  
     1.7 -instance pname::has_pname
     1.8 -by (intro_classes)
     1.9 +instance pname::has_pname ..
    1.10  
    1.11  defs (overloaded)
    1.12  pname_pname_def: "pname (p::pname) \<equiv> p"
    1.13 @@ -80,8 +79,7 @@
    1.14  axclass has_tname < "type"
    1.15  consts tname::"'a::has_tname \<Rightarrow> tname"
    1.16  
    1.17 -instance tname::has_tname
    1.18 -by (intro_classes)
    1.19 +instance tname::has_tname ..
    1.20  
    1.21  defs (overloaded)
    1.22  tname_tname_def: "tname (t::tname) \<equiv> t"
    1.23 @@ -90,8 +88,7 @@
    1.24  consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    1.25  
    1.26  (* Declare qtname as instance of has_qtname *)
    1.27 -instance pid_field_type::(has_pname,"type") has_qtname
    1.28 -by intro_classes 
    1.29 +instance pid_field_type::(has_pname,"type") has_qtname ..
    1.30  
    1.31  defs (overloaded)
    1.32  qtname_qtname_def: "qtname (q::qtname) \<equiv> q"