46 |
46 |
47 record qtname = --{* qualified tname cf. 6.5.3, 6.5.4*} |
47 record qtname = --{* qualified tname cf. 6.5.3, 6.5.4*} |
48 pid :: pname |
48 pid :: pname |
49 tid :: tname |
49 tid :: tname |
50 |
50 |
51 axclass has_pname < "type" |
51 class has_pname = |
52 consts pname::"'a::has_pname \<Rightarrow> pname" |
52 fixes pname :: "'a \<Rightarrow> pname" |
53 |
53 |
54 instance pname::has_pname .. |
54 instantiation pname :: has_pname |
|
55 begin |
55 |
56 |
56 defs (overloaded) |
57 definition |
57 pname_pname_def: "pname (p::pname) \<equiv> p" |
58 pname_pname_def: "pname (p::pname) \<equiv> p" |
58 |
59 |
59 axclass has_tname < "type" |
60 instance .. |
60 consts tname::"'a::has_tname \<Rightarrow> tname" |
|
61 |
61 |
62 instance tname::has_tname .. |
62 end |
63 |
63 |
64 defs (overloaded) |
64 class has_tname = |
65 tname_tname_def: "tname (t::tname) \<equiv> t" |
65 fixes tname :: "'a \<Rightarrow> tname" |
66 |
66 |
67 axclass has_qtname < type |
67 instantiation tname :: has_tname |
68 consts qtname:: "'a::has_qtname \<Rightarrow> qtname" |
68 begin |
69 |
69 |
70 instance qtname_ext_type :: (type) has_qtname .. |
70 definition |
|
71 tname_tname_def: "tname (t::tname) \<equiv> t" |
71 |
72 |
72 defs (overloaded) |
73 instance .. |
73 qtname_qtname_def: "qtname (q::qtname) \<equiv> q" |
74 |
|
75 end |
|
76 |
|
77 definition |
|
78 qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q" |
74 |
79 |
75 translations |
80 translations |
76 "mname" <= "Name.mname" |
81 "mname" <= "Name.mname" |
77 "xname" <= "Name.xname" |
82 "xname" <= "Name.xname" |
78 "tname" <= "Name.tname" |
83 "tname" <= "Name.tname" |