dropped axclass
authorhaftmann
Tue Feb 23 10:11:12 2010 +0100 (2010-02-23)
changeset 35315fbdc860d87a3
parent 35282 8fd9d555d04d
child 35316 870dfea4f9c0
dropped axclass
src/HOL/Algebra/abstract/Ideal2.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/Term.thy
src/HOL/ex/PER.thy
src/HOL/ex/Refute_Examples.thy
src/Pure/Isar/class_target.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ideal2.thy	Mon Feb 22 17:02:39 2010 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ideal2.thy	Tue Feb 23 10:11:12 2010 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4  (*
     1.5      Ideals for commutative rings
     1.6 -    $Id$
     1.7      Author: Clemens Ballarin, started 24 September 1999
     1.8  *)
     1.9  
    1.10 @@ -23,9 +22,8 @@
    1.11  
    1.12  text {* Principle ideal domains *}
    1.13  
    1.14 -axclass pid < "domain"
    1.15 -  pid_ax: "is_ideal I ==> is_pideal I"
    1.16 -
    1.17 +class pid =
    1.18 +  assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
    1.19  
    1.20  (* is_ideal *)
    1.21  
     2.1 --- a/src/HOL/Bali/Decl.thy	Mon Feb 22 17:02:39 2010 +0100
     2.2 +++ b/src/HOL/Bali/Decl.thy	Tue Feb 23 10:11:12 2010 +0100
     2.3 @@ -230,18 +230,22 @@
     2.4  
     2.5  datatype memberid = fid vname | mid sig
     2.6  
     2.7 -axclass has_memberid < "type"
     2.8 -consts
     2.9 - memberid :: "'a::has_memberid \<Rightarrow> memberid"
    2.10 +class has_memberid =
    2.11 +  fixes memberid :: "'a \<Rightarrow> memberid"
    2.12  
    2.13 -instance memberdecl::has_memberid ..
    2.14 +instantiation memberdecl :: has_memberid
    2.15 +begin
    2.16  
    2.17 -defs (overloaded)
    2.18 +definition
    2.19  memberdecl_memberid_def:
    2.20    "memberid m \<equiv> (case m of
    2.21                      fdecl (vn,f)  \<Rightarrow> fid vn
    2.22                    | mdecl (sig,m) \<Rightarrow> mid sig)"
    2.23  
    2.24 +instance ..
    2.25 +
    2.26 +end
    2.27 +
    2.28  lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
    2.29  by (simp add: memberdecl_memberid_def)
    2.30  
    2.31 @@ -254,12 +258,17 @@
    2.32  lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
    2.33  by (cases m) (simp add: memberdecl_memberid_def)
    2.34  
    2.35 -instance * :: (type, has_memberid) has_memberid ..
    2.36 +instantiation * :: (type, has_memberid) has_memberid
    2.37 +begin
    2.38  
    2.39 -defs (overloaded)
    2.40 +definition
    2.41  pair_memberid_def:
    2.42    "memberid p \<equiv> memberid (snd p)"
    2.43  
    2.44 +instance ..
    2.45 +
    2.46 +end
    2.47 +
    2.48  lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
    2.49  by (simp add: pair_memberid_def)
    2.50  
     3.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 22 17:02:39 2010 +0100
     3.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Tue Feb 23 10:11:12 2010 +0100
     3.3 @@ -79,41 +79,60 @@
     3.4  text {* overloaded selector @{text accmodi} to select the access modifier 
     3.5  out of various HOL types *}
     3.6  
     3.7 -axclass has_accmodi < "type"
     3.8 -consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
     3.9 +class has_accmodi =
    3.10 +  fixes accmodi:: "'a \<Rightarrow> acc_modi"
    3.11 +
    3.12 +instantiation acc_modi :: has_accmodi
    3.13 +begin
    3.14  
    3.15 -instance acc_modi::has_accmodi ..
    3.16 +definition
    3.17 +  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    3.18  
    3.19 -defs (overloaded)
    3.20 -acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    3.21 +instance ..
    3.22 +
    3.23 +end
    3.24  
    3.25  lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    3.26  by (simp add: acc_modi_accmodi_def)
    3.27  
    3.28 -instance decl_ext_type:: ("type") has_accmodi ..
    3.29 +instantiation decl_ext_type:: (type) has_accmodi
    3.30 +begin
    3.31  
    3.32 -defs (overloaded)
    3.33 -decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    3.34 +definition
    3.35 +  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    3.36  
    3.37 +instance ..
    3.38 +
    3.39 +end
    3.40  
    3.41  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
    3.42  by (simp add: decl_acc_modi_def)
    3.43  
    3.44 -instance * :: ("type",has_accmodi) has_accmodi ..
    3.45 +instantiation * :: (type, has_accmodi) has_accmodi
    3.46 +begin
    3.47  
    3.48 -defs (overloaded)
    3.49 -pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    3.50 +definition
    3.51 +  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    3.52 +
    3.53 +instance ..
    3.54 +
    3.55 +end
    3.56  
    3.57  lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
    3.58  by (simp add: pair_acc_modi_def)
    3.59  
    3.60 -instance memberdecl :: has_accmodi ..
    3.61 +instantiation memberdecl :: has_accmodi
    3.62 +begin
    3.63  
    3.64 -defs (overloaded)
    3.65 -memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    3.66 +definition
    3.67 +  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    3.68                                            fdecl f \<Rightarrow> accmodi f
    3.69                                          | mdecl m \<Rightarrow> accmodi m)"
    3.70  
    3.71 +instance ..
    3.72 +
    3.73 +end
    3.74 +
    3.75  lemma memberdecl_fdecl_acc_modi_simp[simp]:
    3.76   "accmodi (fdecl m) = accmodi m"
    3.77  by (simp add: memberdecl_acc_modi_def)
    3.78 @@ -125,21 +144,35 @@
    3.79  text {* overloaded selector @{text declclass} to select the declaring class 
    3.80  out of various HOL types *}
    3.81  
    3.82 -axclass has_declclass < "type"
    3.83 -consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
    3.84 +class has_declclass =
    3.85 +  fixes declclass:: "'a \<Rightarrow> qtname"
    3.86 +
    3.87 +instantiation qtname_ext_type :: (type) has_declclass
    3.88 +begin
    3.89  
    3.90 -instance qtname_ext_type::("type") has_declclass ..
    3.91 +definition
    3.92 +  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
    3.93 +
    3.94 +instance ..
    3.95  
    3.96 -defs (overloaded)
    3.97 -qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
    3.98 +end
    3.99 +
   3.100 +lemma qtname_declclass_def:
   3.101 +  "declclass q \<equiv> (q::qtname)"
   3.102 +  by (induct q) (simp add: declclass_qtname_ext_type_def)
   3.103  
   3.104  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
   3.105  by (simp add: qtname_declclass_def)
   3.106  
   3.107 -instance * :: ("has_declclass","type") has_declclass ..
   3.108 +instantiation * :: (has_declclass, type) has_declclass
   3.109 +begin
   3.110  
   3.111 -defs (overloaded)
   3.112 -pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   3.113 +definition
   3.114 +  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
   3.115 +
   3.116 +instance ..
   3.117 +
   3.118 +end
   3.119  
   3.120  lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 
   3.121  by (simp add: pair_declclass_def)
   3.122 @@ -147,25 +180,38 @@
   3.123  text {* overloaded selector @{text is_static} to select the static modifier 
   3.124  out of various HOL types *}
   3.125  
   3.126 +class has_static =
   3.127 +  fixes is_static :: "'a \<Rightarrow> bool"
   3.128  
   3.129 -axclass has_static < "type"
   3.130 -consts is_static :: "'a::has_static \<Rightarrow> bool"
   3.131 +instantiation decl_ext_type :: (has_static) has_static
   3.132 +begin
   3.133  
   3.134 -instance decl_ext_type :: ("has_static") has_static ..
   3.135 +instance ..
   3.136 +
   3.137 +end
   3.138  
   3.139 -instance member_ext_type :: ("type") has_static ..
   3.140 +instantiation member_ext_type :: (type) has_static
   3.141 +begin
   3.142 +
   3.143 +instance ..
   3.144  
   3.145 -defs (overloaded)
   3.146 -static_field_type_is_static_def: 
   3.147 - "is_static (m::('b member_scheme)) \<equiv> static m"
   3.148 +end
   3.149 +
   3.150 +axiomatization where
   3.151 +  static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m"
   3.152  
   3.153  lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
   3.154  by (simp add: static_field_type_is_static_def)
   3.155  
   3.156 -instance * :: ("type","has_static") has_static ..
   3.157 +instantiation * :: (type, has_static) has_static
   3.158 +begin
   3.159  
   3.160 -defs (overloaded)
   3.161 -pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   3.162 +definition
   3.163 +  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
   3.164 +
   3.165 +instance ..
   3.166 +
   3.167 +end
   3.168  
   3.169  lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
   3.170  by (simp add: pair_is_static_def)
   3.171 @@ -173,14 +219,19 @@
   3.172  lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
   3.173  by (simp add: pair_is_static_def)
   3.174  
   3.175 -instance memberdecl:: has_static ..
   3.176 +instantiation memberdecl :: has_static
   3.177 +begin
   3.178  
   3.179 -defs (overloaded)
   3.180 +definition
   3.181  memberdecl_is_static_def: 
   3.182   "is_static m \<equiv> (case m of
   3.183                      fdecl f \<Rightarrow> is_static f
   3.184                    | mdecl m \<Rightarrow> is_static m)"
   3.185  
   3.186 +instance ..
   3.187 +
   3.188 +end
   3.189 +
   3.190  lemma memberdecl_is_static_fdecl_simp[simp]:
   3.191   "is_static (fdecl f) = is_static f"
   3.192  by (simp add: memberdecl_is_static_def)
   3.193 @@ -389,18 +440,32 @@
   3.194  text {* overloaded selector @{text resTy} to select the result type 
   3.195  out of various HOL types *}
   3.196  
   3.197 -axclass has_resTy < "type"
   3.198 -consts resTy:: "'a::has_resTy \<Rightarrow> ty"
   3.199 +class has_resTy =
   3.200 +  fixes resTy:: "'a \<Rightarrow> ty"
   3.201 +
   3.202 +instantiation decl_ext_type :: (has_resTy) has_resTy
   3.203 +begin
   3.204  
   3.205 -instance decl_ext_type :: ("has_resTy") has_resTy ..
   3.206 +instance ..
   3.207 +
   3.208 +end
   3.209 +
   3.210 +instantiation member_ext_type :: (has_resTy) has_resTy
   3.211 +begin
   3.212  
   3.213 -instance member_ext_type :: ("has_resTy") has_resTy ..
   3.214 +instance ..
   3.215  
   3.216 -instance mhead_ext_type :: ("type") has_resTy ..
   3.217 +end
   3.218 +
   3.219 +instantiation mhead_ext_type :: (type) has_resTy
   3.220 +begin
   3.221  
   3.222 -defs (overloaded)
   3.223 -mhead_ext_type_resTy_def: 
   3.224 - "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   3.225 +instance ..
   3.226 +
   3.227 +end
   3.228 +
   3.229 +axiomatization where
   3.230 +  mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m"
   3.231  
   3.232  lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
   3.233  by (simp add: mhead_ext_type_resTy_def)
   3.234 @@ -408,10 +473,15 @@
   3.235  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   3.236  by (simp add: mhead_def mhead_resTy_simp)
   3.237  
   3.238 -instance * :: ("type","has_resTy") has_resTy ..
   3.239 +instantiation * :: ("type","has_resTy") has_resTy
   3.240 +begin
   3.241  
   3.242 -defs (overloaded)
   3.243 -pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   3.244 +definition
   3.245 +  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
   3.246 +
   3.247 +instance ..
   3.248 +
   3.249 +end
   3.250  
   3.251  lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
   3.252  by (simp add: pair_resTy_def)
     4.1 --- a/src/HOL/Bali/Name.thy	Mon Feb 22 17:02:39 2010 +0100
     4.2 +++ b/src/HOL/Bali/Name.thy	Tue Feb 23 10:11:12 2010 +0100
     4.3 @@ -48,29 +48,34 @@
     4.4            pid :: pname  
     4.5            tid :: tname
     4.6  
     4.7 -axclass has_pname < "type"
     4.8 -consts pname::"'a::has_pname \<Rightarrow> pname"
     4.9 +class has_pname =
    4.10 +  fixes pname :: "'a \<Rightarrow> pname"
    4.11  
    4.12 -instance pname::has_pname ..
    4.13 +instantiation pname :: has_pname
    4.14 +begin
    4.15  
    4.16 -defs (overloaded)
    4.17 -pname_pname_def: "pname (p::pname) \<equiv> p"
    4.18 +definition
    4.19 +  pname_pname_def: "pname (p::pname) \<equiv> p"
    4.20  
    4.21 -axclass has_tname < "type"
    4.22 -consts tname::"'a::has_tname \<Rightarrow> tname"
    4.23 +instance ..
    4.24 +
    4.25 +end
    4.26  
    4.27 -instance tname::has_tname ..
    4.28 +class has_tname =
    4.29 +  fixes tname :: "'a \<Rightarrow> tname"
    4.30  
    4.31 -defs (overloaded)
    4.32 -tname_tname_def: "tname (t::tname) \<equiv> t"
    4.33 +instantiation tname :: has_tname
    4.34 +begin
    4.35  
    4.36 -axclass has_qtname < type
    4.37 -consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    4.38 +definition
    4.39 +  tname_tname_def: "tname (t::tname) \<equiv> t"
    4.40 +
    4.41 +instance ..
    4.42  
    4.43 -instance qtname_ext_type :: (type) has_qtname ..
    4.44 +end
    4.45  
    4.46 -defs (overloaded)
    4.47 -qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
    4.48 +definition
    4.49 +  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
    4.50  
    4.51  translations
    4.52    "mname"  <= "Name.mname"
     5.1 --- a/src/HOL/Bali/Term.thy	Mon Feb 22 17:02:39 2010 +0100
     5.2 +++ b/src/HOL/Bali/Term.thy	Tue Feb 23 10:11:12 2010 +0100
     5.3 @@ -295,8 +295,8 @@
     5.4  following.
     5.5  *}
     5.6  
     5.7 -axclass inj_term < "type"
     5.8 -consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
     5.9 +class inj_term =
    5.10 +  fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
    5.11  
    5.12  text {* How this overloaded injections work can be seen in the theory 
    5.13  @{text DefiniteAssignment}. Other big inductive relations on
    5.14 @@ -308,10 +308,15 @@
    5.15  as bridge between the different conventions.  
    5.16  *}
    5.17  
    5.18 -instance stmt::inj_term ..
    5.19 +instantiation stmt :: inj_term
    5.20 +begin
    5.21  
    5.22 -defs (overloaded)
    5.23 -stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    5.24 +definition
    5.25 +  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    5.26 +
    5.27 +instance ..
    5.28 +
    5.29 +end
    5.30  
    5.31  lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    5.32  by (simp add: stmt_inj_term_def)
    5.33 @@ -319,10 +324,15 @@
    5.34  lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    5.35    by (simp add: stmt_inj_term_simp)
    5.36  
    5.37 -instance expr::inj_term ..
    5.38 +instantiation expr :: inj_term
    5.39 +begin
    5.40  
    5.41 -defs (overloaded)
    5.42 -expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    5.43 +definition
    5.44 +  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    5.45 +
    5.46 +instance ..
    5.47 +
    5.48 +end
    5.49  
    5.50  lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    5.51  by (simp add: expr_inj_term_def)
    5.52 @@ -330,10 +340,15 @@
    5.53  lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    5.54    by (simp add: expr_inj_term_simp)
    5.55  
    5.56 -instance var::inj_term ..
    5.57 +instantiation var :: inj_term
    5.58 +begin
    5.59  
    5.60 -defs (overloaded)
    5.61 -var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    5.62 +definition
    5.63 +  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    5.64 +
    5.65 +instance ..
    5.66 +
    5.67 +end
    5.68  
    5.69  lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
    5.70  by (simp add: var_inj_term_def)
    5.71 @@ -341,10 +356,32 @@
    5.72  lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    5.73    by (simp add: var_inj_term_simp)
    5.74  
    5.75 -instance "list":: (type) inj_term ..
    5.76 +class expr_of =
    5.77 +  fixes expr_of :: "'a \<Rightarrow> expr"
    5.78 +
    5.79 +instantiation expr :: expr_of
    5.80 +begin
    5.81 +
    5.82 +definition
    5.83 +  "expr_of = (\<lambda>(e::expr). e)"
    5.84 +
    5.85 +instance ..
    5.86 +
    5.87 +end 
    5.88  
    5.89 -defs (overloaded)
    5.90 -expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
    5.91 +instantiation list :: (expr_of) inj_term
    5.92 +begin
    5.93 +
    5.94 +definition
    5.95 +  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
    5.96 +
    5.97 +instance ..
    5.98 +
    5.99 +end
   5.100 +
   5.101 +lemma expr_list_inj_term_def:
   5.102 +  "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   5.103 +  by (simp add: inj_term_list_def expr_of_expr_def)
   5.104  
   5.105  lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   5.106  by (simp add: expr_list_inj_term_def)
     6.1 --- a/src/HOL/ex/PER.thy	Mon Feb 22 17:02:39 2010 +0100
     6.2 +++ b/src/HOL/ex/PER.thy	Tue Feb 23 10:11:12 2010 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/ex/PER.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
     6.7  *)
     6.8  
     6.9 @@ -30,12 +29,10 @@
    6.10    but not necessarily reflexive.
    6.11  *}
    6.12  
    6.13 -consts
    6.14 -  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
    6.15 -
    6.16 -axclass partial_equiv < type
    6.17 -  partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    6.18 -  partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    6.19 +class partial_equiv =
    6.20 +  fixes eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
    6.21 +  assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
    6.22 +  assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
    6.23  
    6.24  text {*
    6.25    \medskip The domain of a partial equivalence relation is the set of
    6.26 @@ -70,7 +67,10 @@
    6.27    structural one corresponding to the congruence property.
    6.28  *}
    6.29  
    6.30 -defs (overloaded)
    6.31 +instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
    6.32 +begin
    6.33 +
    6.34 +definition
    6.35    eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
    6.36  
    6.37  lemma partial_equiv_funI [intro?]:
    6.38 @@ -86,8 +86,7 @@
    6.39    spaces (in \emph{both} argument positions).
    6.40  *}
    6.41  
    6.42 -instance "fun" :: (partial_equiv, partial_equiv) partial_equiv
    6.43 -proof
    6.44 +instance proof
    6.45    fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
    6.46    assume fg: "f \<sim> g"
    6.47    show "g \<sim> f"
    6.48 @@ -110,6 +109,8 @@
    6.49    qed
    6.50  qed
    6.51  
    6.52 +end
    6.53 +
    6.54  
    6.55  subsection {* Total equivalence *}
    6.56  
    6.57 @@ -120,8 +121,8 @@
    6.58    symmetric.
    6.59  *}
    6.60  
    6.61 -axclass equiv < partial_equiv
    6.62 -  eqv_refl [intro]: "x \<sim> x"
    6.63 +class equiv =
    6.64 +  assumes eqv_refl [intro]: "x \<sim> x"
    6.65  
    6.66  text {*
    6.67    On total equivalences all elements are reflexive, and congruence
    6.68 @@ -150,7 +151,7 @@
    6.69    \emph{equivalence classes} over elements of the base type @{typ 'a}.
    6.70  *}
    6.71  
    6.72 -typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
    6.73 +typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
    6.74    by blast
    6.75  
    6.76  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
     7.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Feb 22 17:02:39 2010 +0100
     7.2 +++ b/src/HOL/ex/Refute_Examples.thy	Tue Feb 23 10:11:12 2010 +0100
     7.3 @@ -1417,29 +1417,20 @@
     7.4  
     7.5  (*****************************************************************************)
     7.6  
     7.7 -subsubsection {* Axiomatic type classes and overloading *}
     7.8 +subsubsection {* Type classes and overloading *}
     7.9  
    7.10  text {* A type class without axioms: *}
    7.11  
    7.12 -axclass classA
    7.13 +class classA
    7.14  
    7.15  lemma "P (x::'a::classA)"
    7.16    refute
    7.17  oops
    7.18  
    7.19 -text {* The axiom of this type class does not contain any type variables: *}
    7.20 -
    7.21 -axclass classB
    7.22 -  classB_ax: "P | ~ P"
    7.23 -
    7.24 -lemma "P (x::'a::classB)"
    7.25 -  refute
    7.26 -oops
    7.27 -
    7.28  text {* An axiom with a type variable (denoting types which have at least two elements): *}
    7.29  
    7.30 -axclass classC < type
    7.31 -  classC_ax: "\<exists>x y. x \<noteq> y"
    7.32 +class classC =
    7.33 +  assumes classC_ax: "\<exists>x y. x \<noteq> y"
    7.34  
    7.35  lemma "P (x::'a::classC)"
    7.36    refute
    7.37 @@ -1451,11 +1442,9 @@
    7.38  
    7.39  text {* A type class for which a constant is defined: *}
    7.40  
    7.41 -consts
    7.42 -  classD_const :: "'a \<Rightarrow> 'a"
    7.43 -
    7.44 -axclass classD < type
    7.45 -  classD_ax: "classD_const (classD_const x) = classD_const x"
    7.46 +class classD =
    7.47 +  fixes classD_const :: "'a \<Rightarrow> 'a"
    7.48 +  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
    7.49  
    7.50  lemma "P (x::'a::classD)"
    7.51    refute
    7.52 @@ -1463,16 +1452,12 @@
    7.53  
    7.54  text {* A type class with multiple superclasses: *}
    7.55  
    7.56 -axclass classE < classC, classD
    7.57 +class classE = classC + classD
    7.58  
    7.59  lemma "P (x::'a::classE)"
    7.60    refute
    7.61  oops
    7.62  
    7.63 -lemma "P (x::'a::{classB, classE})"
    7.64 -  refute
    7.65 -oops
    7.66 -
    7.67  text {* OFCLASS: *}
    7.68  
    7.69  lemma "OFCLASS('a::type, type_class)"
    7.70 @@ -1485,12 +1470,6 @@
    7.71    apply intro_classes
    7.72  done
    7.73  
    7.74 -lemma "OFCLASS('a, classB_class)"
    7.75 -  refute  -- {* no countermodel exists *}
    7.76 -  apply intro_classes
    7.77 -  apply simp
    7.78 -done
    7.79 -
    7.80  lemma "OFCLASS('a::type, classC_class)"
    7.81    refute
    7.82  oops
     8.1 --- a/src/Pure/Isar/class_target.ML	Mon Feb 22 17:02:39 2010 +0100
     8.2 +++ b/src/Pure/Isar/class_target.ML	Tue Feb 23 10:11:12 2010 +0100
     8.3 @@ -56,11 +56,6 @@
     8.4    (*tactics*)
     8.5    val intro_classes_tac: thm list -> tactic
     8.6    val default_intro_tac: Proof.context -> thm list -> tactic
     8.7 -
     8.8 -  (*old axclass layer*)
     8.9 -  val axclass_cmd: binding * xstring list
    8.10 -    -> (Attrib.binding * string list) list
    8.11 -    -> theory -> class * theory
    8.12  end;
    8.13  
    8.14  structure Class_Target : CLASS_TARGET =
    8.15 @@ -629,24 +624,5 @@
    8.16    Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
    8.17      "apply some intro/elim rule"));
    8.18  
    8.19 -
    8.20 -(** old axclass command **)
    8.21 -
    8.22 -fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    8.23 -  let
    8.24 -    val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead.";
    8.25 -    val ctxt = ProofContext.init thy;
    8.26 -    val superclasses = map (Sign.read_class thy) raw_superclasses;
    8.27 -    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
    8.28 -      raw_specs;
    8.29 -    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
    8.30 -          raw_specs)
    8.31 -      |> snd
    8.32 -      |> (map o map) fst;
    8.33 -  in
    8.34 -    AxClass.define_class (class, superclasses) []
    8.35 -      (name_atts ~~ axiomss) thy
    8.36 -  end;
    8.37 -
    8.38  end;
    8.39  
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 22 17:02:39 2010 +0100
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 23 10:11:12 2010 +0100
     9.3 @@ -99,13 +99,6 @@
     9.4    OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
     9.5      (P.sort >> (Toplevel.theory o Sign.add_defsort));
     9.6  
     9.7 -val _ =
     9.8 -  OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
     9.9 -    (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    9.10 -        P.!!! (P.list1 P.xname)) []
    9.11 -        -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    9.12 -      >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
    9.13 -
    9.14  
    9.15  (* types *)
    9.16