changeset 14700 | 2f885b7e5ba7 |
parent 13688 | a0b16d42d489 |
child 14981 | e73f8140af78 |
--- a/src/HOL/Bali/Name.thy Sat May 01 22:28:51 2004 +0200 +++ b/src/HOL/Bali/Name.thy Mon May 03 23:22:17 2004 +0200 @@ -80,7 +80,7 @@ consts qtname:: "'a::has_qtname \<Rightarrow> qtname" (* Declare qtname as instance of has_qtname *) -instance pid_field_type::(has_pname,"type") has_qtname .. +instance qtname_ext_type::("type") has_qtname .. defs (overloaded) qtname_qtname_def: "qtname (q::qtname) \<equiv> q"