src/HOL/Bali/DeclConcepts.thy
changeset 12859 f63315dfffd4
parent 12854 00d4a435777f
child 12925 99131847fb93
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Jan 28 18:51:48 2002 +0100
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Jan 28 23:35:20 2002 +0100
     1.3 @@ -79,8 +79,7 @@
     1.4  axclass has_accmodi < "type"
     1.5  consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
     1.6  
     1.7 -instance acc_modi::has_accmodi
     1.8 -by (intro_classes)
     1.9 +instance acc_modi::has_accmodi ..
    1.10  
    1.11  defs (overloaded)
    1.12  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    1.13 @@ -88,8 +87,7 @@
    1.14  lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    1.15  by (simp add: acc_modi_accmodi_def)
    1.16  
    1.17 -instance access_field_type:: ("type","type") has_accmodi
    1.18 -by (intro_classes)
    1.19 +instance access_field_type:: ("type","type") has_accmodi ..
    1.20  
    1.21  defs (overloaded)
    1.22  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    1.23 @@ -98,8 +96,7 @@
    1.24  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
    1.25  by (simp add: decl_acc_modi_def)
    1.26  
    1.27 -instance * :: ("type",has_accmodi) has_accmodi
    1.28 -by (intro_classes)
    1.29 +instance * :: ("type",has_accmodi) has_accmodi ..
    1.30  
    1.31  defs (overloaded)
    1.32  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    1.33 @@ -107,8 +104,7 @@
    1.34  lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
    1.35  by (simp add: pair_acc_modi_def)
    1.36  
    1.37 -instance memberdecl :: has_accmodi
    1.38 -by (intro_classes)
    1.39 +instance memberdecl :: has_accmodi ..
    1.40  
    1.41  defs (overloaded)
    1.42  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    1.43 @@ -129,8 +125,7 @@
    1.44  axclass has_declclass < "type"
    1.45  consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
    1.46  
    1.47 -instance pid_field_type::("type","type") has_declclass
    1.48 -by (intro_classes)
    1.49 +instance pid_field_type::("type","type") has_declclass ..
    1.50  
    1.51  defs (overloaded)
    1.52  qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
    1.53 @@ -138,8 +133,7 @@
    1.54  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
    1.55  by (simp add: qtname_declclass_def)
    1.56  
    1.57 -instance * :: ("has_declclass","type") has_declclass
    1.58 -by (intro_classes)
    1.59 +instance * :: ("has_declclass","type") has_declclass ..
    1.60  
    1.61  defs (overloaded)
    1.62  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
    1.63 @@ -158,15 +152,13 @@
    1.64  consts is_static :: "'a \<Rightarrow> bool"
    1.65  *)
    1.66  
    1.67 -instance access_field_type :: ("type","has_static") has_static
    1.68 -by (intro_classes) 
    1.69 +instance access_field_type :: ("type","has_static") has_static ..
    1.70  
    1.71  defs (overloaded)
    1.72  decl_is_static_def: 
    1.73   "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
    1.74  
    1.75 -instance static_field_type :: ("type","type") has_static
    1.76 -by (intro_classes)
    1.77 +instance static_field_type :: ("type","type") has_static ..
    1.78  
    1.79  defs (overloaded)
    1.80  static_field_type_is_static_def: 
    1.81 @@ -178,8 +170,7 @@
    1.82                   decl_is_static_def Decl.member.dest_convs)
    1.83  done
    1.84  
    1.85 -instance * :: ("type","has_static") has_static
    1.86 -by (intro_classes)
    1.87 +instance * :: ("type","has_static") has_static ..
    1.88  
    1.89  defs (overloaded)
    1.90  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
    1.91 @@ -190,8 +181,7 @@
    1.92  lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
    1.93  by (simp add: pair_is_static_def)
    1.94  
    1.95 -instance memberdecl:: has_static
    1.96 -by (intro_classes)
    1.97 +instance memberdecl:: has_static ..
    1.98  
    1.99  defs (overloaded)
   1.100  memberdecl_is_static_def: 
   1.101 @@ -432,31 +422,27 @@
   1.102  axclass has_resTy < "type"
   1.103  consts resTy:: "'a::has_resTy \<Rightarrow> ty"
   1.104  
   1.105 -instance access_field_type :: ("type","has_resTy") has_resTy
   1.106 -by (intro_classes)
   1.107 +instance access_field_type :: ("type","has_resTy") has_resTy ..
   1.108  
   1.109  defs (overloaded)
   1.110  decl_resTy_def: 
   1.111   "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
   1.112  
   1.113 -instance static_field_type :: ("type","has_resTy") has_resTy
   1.114 -by (intro_classes)
   1.115 +instance static_field_type :: ("type","has_resTy") has_resTy ..
   1.116  
   1.117  defs (overloaded)
   1.118  static_field_type_resTy_def: 
   1.119   "resTy (m::(bool,'b::has_resTy) static_field_type) 
   1.120    \<equiv> resTy (static_more m)" 
   1.121  
   1.122 -instance pars_field_type :: ("type","has_resTy") has_resTy
   1.123 -by (intro_classes)
   1.124 +instance pars_field_type :: ("type","has_resTy") has_resTy ..
   1.125  
   1.126  defs (overloaded)
   1.127  pars_field_type_resTy_def: 
   1.128   "resTy (m::(vname list,'b::has_resTy) pars_field_type) 
   1.129    \<equiv> resTy (pars_more m)" 
   1.130  
   1.131 -instance resT_field_type :: ("type","type") has_resTy
   1.132 -by (intro_classes)
   1.133 +instance resT_field_type :: ("type","type") has_resTy ..
   1.134  
   1.135  defs (overloaded)
   1.136  resT_field_type_resTy_def: 
   1.137 @@ -473,8 +459,7 @@
   1.138  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   1.139  by (simp add: mhead_def mhead_resTy_simp)
   1.140  
   1.141 -instance * :: ("type","has_resTy") has_resTy
   1.142 -by (intro_classes)
   1.143 +instance * :: ("type","has_resTy") has_resTy ..
   1.144  
   1.145  defs (overloaded)
   1.146  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"