Ported HOL and HOL-Library to new locales.
authorballarin
Sun Dec 14 18:45:51 2008 +0100 (2008-12-14)
changeset 29233ce6d35a0bed6
parent 29232 712c5281d4a4
child 29234 60f7fb56f8cd
Ported HOL and HOL-Library to new locales.
src/HOL/Complex.thy
src/HOL/FrechetDeriv.thy
src/HOL/Groebner_Basis.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/ROOT.ML
src/HOL/Real/RealVector.thy
src/HOL/ex/LocaleTest2.thy
     1.1 --- a/src/HOL/Complex.thy	Sun Dec 14 18:45:16 2008 +0100
     1.2 +++ b/src/HOL/Complex.thy	Sun Dec 14 18:45:51 2008 +0100
     1.3 @@ -345,13 +345,13 @@
     1.4  
     1.5  subsection {* Completeness of the Complexes *}
     1.6  
     1.7 -interpretation Re: bounded_linear ["Re"]
     1.8 +interpretation Re!: bounded_linear "Re"
     1.9  apply (unfold_locales, simp, simp)
    1.10  apply (rule_tac x=1 in exI)
    1.11  apply (simp add: complex_norm_def)
    1.12  done
    1.13  
    1.14 -interpretation Im: bounded_linear ["Im"]
    1.15 +interpretation Im!: bounded_linear "Im"
    1.16  apply (unfold_locales, simp, simp)
    1.17  apply (rule_tac x=1 in exI)
    1.18  apply (simp add: complex_norm_def)
    1.19 @@ -513,7 +513,7 @@
    1.20  lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
    1.21  by (simp add: norm_mult power2_eq_square)
    1.22  
    1.23 -interpretation cnj: bounded_linear ["cnj"]
    1.24 +interpretation cnj!: bounded_linear "cnj"
    1.25  apply (unfold_locales)
    1.26  apply (rule complex_cnj_add)
    1.27  apply (rule complex_cnj_scaleR)
     2.1 --- a/src/HOL/FrechetDeriv.thy	Sun Dec 14 18:45:16 2008 +0100
     2.2 +++ b/src/HOL/FrechetDeriv.thy	Sun Dec 14 18:45:51 2008 +0100
     2.3 @@ -65,8 +65,8 @@
     2.4    assumes "bounded_linear g"
     2.5    shows "bounded_linear (\<lambda>x. f x + g x)"
     2.6  proof -
     2.7 -  interpret f: bounded_linear [f] by fact
     2.8 -  interpret g: bounded_linear [g] by fact
     2.9 +  interpret f: bounded_linear f by fact
    2.10 +  interpret g: bounded_linear g by fact
    2.11    show ?thesis apply (unfold_locales)
    2.12      apply (simp only: f.add g.add add_ac)
    2.13      apply (simp only: f.scaleR g.scaleR scaleR_right_distrib)
    2.14 @@ -124,7 +124,7 @@
    2.15    assumes "bounded_linear f"
    2.16    shows "bounded_linear (\<lambda>x. - f x)"
    2.17  proof -
    2.18 -  interpret f: bounded_linear [f] by fact
    2.19 +  interpret f: bounded_linear f by fact
    2.20    show ?thesis apply (unfold_locales)
    2.21      apply (simp add: f.add)
    2.22      apply (simp add: f.scaleR)
    2.23 @@ -151,7 +151,7 @@
    2.24    assumes f: "FDERIV f x :> F"
    2.25    shows "isCont f x"
    2.26  proof -
    2.27 -  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
    2.28 +  from f interpret F: bounded_linear "F" by (rule FDERIV_bounded_linear)
    2.29    have "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h) -- 0 --> 0"
    2.30      by (rule FDERIV_D [OF f])
    2.31    hence "(\<lambda>h. norm (f (x + h) - f x - F h) / norm h * norm h) -- 0 --> 0"
    2.32 @@ -180,8 +180,8 @@
    2.33    assumes "bounded_linear g"
    2.34    shows "bounded_linear (\<lambda>x. f (g x))"
    2.35  proof -
    2.36 -  interpret f: bounded_linear [f] by fact
    2.37 -  interpret g: bounded_linear [g] by fact
    2.38 +  interpret f: bounded_linear f by fact
    2.39 +  interpret g: bounded_linear g by fact
    2.40    show ?thesis proof (unfold_locales)
    2.41      fix x y show "f (g (x + y)) = f (g x) + f (g y)"
    2.42        by (simp only: f.add g.add)
    2.43 @@ -223,8 +223,8 @@
    2.44    let ?k = "\<lambda>h. f (x + h) - f x"
    2.45    let ?Nf = "\<lambda>h. norm (?Rf h) / norm h"
    2.46    let ?Ng = "\<lambda>h. norm (?Rg (?k h)) / norm (?k h)"
    2.47 -  from f interpret F: bounded_linear ["F"] by (rule FDERIV_bounded_linear)
    2.48 -  from g interpret G: bounded_linear ["G"] by (rule FDERIV_bounded_linear)
    2.49 +  from f interpret F!: bounded_linear "F" by (rule FDERIV_bounded_linear)
    2.50 +  from g interpret G!: bounded_linear "G" by (rule FDERIV_bounded_linear)
    2.51    from F.bounded obtain kF where kF: "\<And>x. norm (F x) \<le> norm x * kF" by fast
    2.52    from G.bounded obtain kG where kG: "\<And>x. norm (G x) \<le> norm x * kG" by fast
    2.53  
    2.54 @@ -375,9 +375,9 @@
    2.55      by (simp only: FDERIV_lemma)
    2.56  qed
    2.57  
    2.58 -lemmas FDERIV_mult = bounded_bilinear_locale.mult.prod.FDERIV
    2.59 +lemmas FDERIV_mult = mult.FDERIV
    2.60  
    2.61 -lemmas FDERIV_scaleR = bounded_bilinear_locale.scaleR.prod.FDERIV
    2.62 +lemmas FDERIV_scaleR = scaleR.FDERIV
    2.63  
    2.64  
    2.65  subsection {* Powers *}
    2.66 @@ -409,10 +409,10 @@
    2.67  by (simp add: right_diff_distrib left_diff_distrib mult_assoc)
    2.68  
    2.69  lemmas bounded_linear_mult_const =
    2.70 -  bounded_bilinear_locale.mult.prod.bounded_linear_left [THEN bounded_linear_compose]
    2.71 +  mult.bounded_linear_left [THEN bounded_linear_compose]
    2.72  
    2.73  lemmas bounded_linear_const_mult =
    2.74 -  bounded_bilinear_locale.mult.prod.bounded_linear_right [THEN bounded_linear_compose]
    2.75 +  mult.bounded_linear_right [THEN bounded_linear_compose]
    2.76  
    2.77  lemma FDERIV_inverse:
    2.78    fixes x :: "'a::real_normed_div_algebra"
    2.79 @@ -492,7 +492,7 @@
    2.80    fixes x :: "'a::real_normed_field" shows
    2.81    "FDERIV f x :> (\<lambda>h. h * D) = (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
    2.82   apply (unfold fderiv_def)
    2.83 - apply (simp add: bounded_bilinear_locale.mult.prod.bounded_linear_left)
    2.84 + apply (simp add: mult.bounded_linear_left)
    2.85   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
    2.86   apply (subst diff_divide_distrib)
    2.87   apply (subst times_divide_eq_left [symmetric])
     3.1 --- a/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:16 2008 +0100
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Dec 14 18:45:51 2008 +0100
     3.3 @@ -163,7 +163,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -interpretation class_semiring: gb_semiring
     3.8 +interpretation class_semiring!: gb_semiring
     3.9      "op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"
    3.10    proof qed (auto simp add: ring_simps power_Suc)
    3.11  
    3.12 @@ -242,7 +242,7 @@
    3.13  end
    3.14  
    3.15  
    3.16 -interpretation class_ring: gb_ring "op +" "op *" "op ^"
    3.17 +interpretation class_ring!: gb_ring "op +" "op *" "op ^"
    3.18      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"
    3.19    proof qed simp_all
    3.20  
    3.21 @@ -343,7 +343,7 @@
    3.22    thus "b = 0" by blast
    3.23  qed
    3.24  
    3.25 -interpretation class_ringb: ringb
    3.26 +interpretation class_ringb!: ringb
    3.27    "op +" "op *" "op ^" "0::'a::{idom,recpower,number_ring}" "1" "op -" "uminus"
    3.28  proof(unfold_locales, simp add: ring_simps power_Suc, auto)
    3.29    fix w x y z ::"'a::{idom,recpower,number_ring}"
    3.30 @@ -359,7 +359,7 @@
    3.31  
    3.32  declaration {* normalizer_funs @{thm class_ringb.ringb_axioms'} *}
    3.33  
    3.34 -interpretation natgb: semiringb
    3.35 +interpretation natgb!: semiringb
    3.36    "op +" "op *" "op ^" "0::nat" "1"
    3.37  proof (unfold_locales, simp add: ring_simps power_Suc)
    3.38    fix w x y z ::"nat"
    3.39 @@ -464,7 +464,7 @@
    3.40  
    3.41  subsection{* Groebner Bases for fields *}
    3.42  
    3.43 -interpretation class_fieldgb:
    3.44 +interpretation class_fieldgb!:
    3.45    fieldgb "op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse" apply (unfold_locales) by (simp_all add: divide_inverse)
    3.46  
    3.47  lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp
     4.1 --- a/src/HOL/Library/Multiset.thy	Sun Dec 14 18:45:16 2008 +0100
     4.2 +++ b/src/HOL/Library/Multiset.thy	Sun Dec 14 18:45:51 2008 +0100
     4.3 @@ -1080,15 +1080,15 @@
     4.4  apply simp
     4.5  done
     4.6  
     4.7 -interpretation mset_order: order ["op \<le>#" "op <#"]
     4.8 +class_interpretation mset_order: order ["op \<le>#" "op <#"]
     4.9  proof qed (auto intro: order.intro mset_le_refl mset_le_antisym
    4.10    mset_le_trans simp: mset_less_def)
    4.11  
    4.12 -interpretation mset_order_cancel_semigroup:
    4.13 +class_interpretation mset_order_cancel_semigroup:
    4.14    pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
    4.15  proof qed (erule mset_le_mono_add [OF mset_le_refl])
    4.16  
    4.17 -interpretation mset_order_semigroup_cancel:
    4.18 +class_interpretation mset_order_semigroup_cancel:
    4.19    pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
    4.20  proof qed simp
    4.21  
    4.22 @@ -1404,7 +1404,7 @@
    4.23    assumes "left_commutative g"
    4.24    shows "(\<And>x y. h (g x y) = f x (h y)) \<Longrightarrow> h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P")
    4.25  proof -
    4.26 -  interpret left_commutative [g] by fact
    4.27 +  interpret left_commutative g by fact
    4.28    show "PROP ?P" by (induct A) auto
    4.29  qed
    4.30  
    4.31 @@ -1436,7 +1436,7 @@
    4.32  definition [code del]:
    4.33   "image_mset f = fold_mset (op + o single o f) {#}"
    4.34  
    4.35 -interpretation image_left_comm: left_commutative ["op + o single o f"]
    4.36 +interpretation image_left_comm!: left_commutative "op + o single o f"
    4.37    proof qed (simp add:union_ac)
    4.38  
    4.39  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
     5.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Sun Dec 14 18:45:16 2008 +0100
     5.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Sun Dec 14 18:45:51 2008 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Library/SetsAndFunctions.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Jeremy Avigad and Kevin Donnelly
     5.7  *)
     5.8  
     5.9 @@ -108,26 +107,26 @@
    5.10    apply simp
    5.11    done
    5.12  
    5.13 -interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
    5.14 +class_interpretation set_semigroup_add: semigroup_add ["op \<oplus> :: ('a::semigroup_add) set => 'a set => 'a set"]
    5.15    apply default
    5.16    apply (unfold set_plus_def)
    5.17    apply (force simp add: add_assoc)
    5.18    done
    5.19  
    5.20 -interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
    5.21 +class_interpretation set_semigroup_mult: semigroup_mult ["op \<otimes> :: ('a::semigroup_mult) set => 'a set => 'a set"]
    5.22    apply default
    5.23    apply (unfold set_times_def)
    5.24    apply (force simp add: mult_assoc)
    5.25    done
    5.26  
    5.27 -interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
    5.28 +class_interpretation set_comm_monoid_add: comm_monoid_add ["{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"]
    5.29    apply default
    5.30     apply (unfold set_plus_def)
    5.31     apply (force simp add: add_ac)
    5.32    apply force
    5.33    done
    5.34  
    5.35 -interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
    5.36 +class_interpretation set_comm_monoid_mult: comm_monoid_mult ["{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"]
    5.37    apply default
    5.38     apply (unfold set_times_def)
    5.39     apply (force simp add: mult_ac)
     6.1 --- a/src/HOL/ROOT.ML	Sun Dec 14 18:45:16 2008 +0100
     6.2 +++ b/src/HOL/ROOT.ML	Sun Dec 14 18:45:51 2008 +0100
     6.3 @@ -3,6 +3,7 @@
     6.4  Classical Higher-order Logic -- batteries included.
     6.5  *)
     6.6  
     6.7 +set new_locales;
     6.8  use_thy "Complex_Main";
     6.9  
    6.10  val HOL_proofs = ! Proofterm.proofs;
     7.1 --- a/src/HOL/Real/RealVector.thy	Sun Dec 14 18:45:16 2008 +0100
     7.2 +++ b/src/HOL/Real/RealVector.thy	Sun Dec 14 18:45:51 2008 +0100
     7.3 @@ -151,7 +151,7 @@
     7.4    and scaleR_scaleR [simp]: "scaleR a (scaleR b x) = scaleR (a * b) x"
     7.5    and scaleR_one [simp]: "scaleR 1 x = x"
     7.6  
     7.7 -interpretation real_vector:
     7.8 +interpretation real_vector!:
     7.9    vector_space "scaleR :: real \<Rightarrow> 'a \<Rightarrow> 'a::real_vector"
    7.10  apply unfold_locales
    7.11  apply (rule scaleR_right_distrib)
    7.12 @@ -195,10 +195,10 @@
    7.13  apply (rule mult_left_commute)
    7.14  done
    7.15  
    7.16 -interpretation scaleR_left: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
    7.17 +interpretation scaleR_left!: additive "(\<lambda>a. scaleR a x::'a::real_vector)"
    7.18  proof qed (rule scaleR_left_distrib)
    7.19  
    7.20 -interpretation scaleR_right: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
    7.21 +interpretation scaleR_right!: additive "(\<lambda>x. scaleR a x::'a::real_vector)"
    7.22  proof qed (rule scaleR_right_distrib)
    7.23  
    7.24  lemma nonzero_inverse_scaleR_distrib:
    7.25 @@ -796,7 +796,7 @@
    7.26  
    7.27  end
    7.28  
    7.29 -interpretation mult:
    7.30 +interpretation mult!:
    7.31    bounded_bilinear "op * :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra"
    7.32  apply (rule bounded_bilinear.intro)
    7.33  apply (rule left_distrib)
    7.34 @@ -807,19 +807,19 @@
    7.35  apply (simp add: norm_mult_ineq)
    7.36  done
    7.37  
    7.38 -interpretation mult_left:
    7.39 +interpretation mult_left!:
    7.40    bounded_linear "(\<lambda>x::'a::real_normed_algebra. x * y)"
    7.41  by (rule mult.bounded_linear_left)
    7.42  
    7.43 -interpretation mult_right:
    7.44 +interpretation mult_right!:
    7.45    bounded_linear "(\<lambda>y::'a::real_normed_algebra. x * y)"
    7.46  by (rule mult.bounded_linear_right)
    7.47  
    7.48 -interpretation divide:
    7.49 +interpretation divide!:
    7.50    bounded_linear "(\<lambda>x::'a::real_normed_field. x / y)"
    7.51  unfolding divide_inverse by (rule mult.bounded_linear_left)
    7.52  
    7.53 -interpretation scaleR: bounded_bilinear "scaleR"
    7.54 +interpretation scaleR!: bounded_bilinear "scaleR"
    7.55  apply (rule bounded_bilinear.intro)
    7.56  apply (rule scaleR_left_distrib)
    7.57  apply (rule scaleR_right_distrib)
    7.58 @@ -829,13 +829,13 @@
    7.59  apply (simp add: norm_scaleR)
    7.60  done
    7.61  
    7.62 -interpretation scaleR_left: bounded_linear "\<lambda>r. scaleR r x"
    7.63 +interpretation scaleR_left!: bounded_linear "\<lambda>r. scaleR r x"
    7.64  by (rule scaleR.bounded_linear_left)
    7.65  
    7.66 -interpretation scaleR_right: bounded_linear "\<lambda>x. scaleR r x"
    7.67 +interpretation scaleR_right!: bounded_linear "\<lambda>x. scaleR r x"
    7.68  by (rule scaleR.bounded_linear_right)
    7.69  
    7.70 -interpretation of_real: bounded_linear "\<lambda>r. of_real r"
    7.71 +interpretation of_real!: bounded_linear "\<lambda>r. of_real r"
    7.72  unfolding of_real_def by (rule scaleR.bounded_linear_left)
    7.73  
    7.74  end
     8.1 --- a/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:16 2008 +0100
     8.2 +++ b/src/HOL/ex/LocaleTest2.thy	Sun Dec 14 18:45:51 2008 +0100
     8.3 @@ -468,7 +468,7 @@
     8.4  
     8.5  subsubsection {* Total order @{text "<="} on @{typ int} *}
     8.6  
     8.7 -interpretation int: dpo "op <= :: [int, int] => bool"
     8.8 +interpretation int!: dpo "op <= :: [int, int] => bool"
     8.9    where "(dpo.less (op <=) (x::int) y) = (x < y)"
    8.10    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
    8.11  proof -
    8.12 @@ -487,7 +487,7 @@
    8.13  lemma "(op < :: [int, int] => bool) = op <"
    8.14    apply (rule int.abs_test) done
    8.15  
    8.16 -interpretation int: dlat "op <= :: [int, int] => bool"
    8.17 +interpretation int!: dlat "op <= :: [int, int] => bool"
    8.18    where meet_eq: "dlat.meet (op <=) (x::int) y = min x y"
    8.19      and join_eq: "dlat.join (op <=) (x::int) y = max x y"
    8.20  proof -
    8.21 @@ -511,7 +511,7 @@
    8.22      by auto
    8.23  qed
    8.24  
    8.25 -interpretation int: dlo "op <= :: [int, int] => bool"
    8.26 +interpretation int!: dlo "op <= :: [int, int] => bool"
    8.27    proof qed arith
    8.28  
    8.29  text {* Interpreted theorems from the locales, involving defined terms. *}
    8.30 @@ -524,7 +524,7 @@
    8.31  
    8.32  subsubsection {* Total order @{text "<="} on @{typ nat} *}
    8.33  
    8.34 -interpretation nat: dpo "op <= :: [nat, nat] => bool"
    8.35 +interpretation nat!: dpo "op <= :: [nat, nat] => bool"
    8.36    where "dpo.less (op <=) (x::nat) y = (x < y)"
    8.37    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
    8.38  proof -
    8.39 @@ -538,7 +538,7 @@
    8.40      done
    8.41  qed
    8.42  
    8.43 -interpretation nat: dlat "op <= :: [nat, nat] => bool"
    8.44 +interpretation nat!: dlat "op <= :: [nat, nat] => bool"
    8.45    where "dlat.meet (op <=) (x::nat) y = min x y"
    8.46      and "dlat.join (op <=) (x::nat) y = max x y"
    8.47  proof -
    8.48 @@ -562,7 +562,7 @@
    8.49      by auto
    8.50  qed
    8.51  
    8.52 -interpretation nat: dlo "op <= :: [nat, nat] => bool"
    8.53 +interpretation nat!: dlo "op <= :: [nat, nat] => bool"
    8.54    proof qed arith
    8.55  
    8.56  text {* Interpreted theorems from the locales, involving defined terms. *}
    8.57 @@ -575,7 +575,7 @@
    8.58  
    8.59  subsubsection {* Lattice @{text "dvd"} on @{typ nat} *}
    8.60  
    8.61 -interpretation nat_dvd: dpo "op dvd :: [nat, nat] => bool"
    8.62 +interpretation nat_dvd!: dpo "op dvd :: [nat, nat] => bool"
    8.63    where "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
    8.64    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
    8.65  proof -
    8.66 @@ -589,7 +589,7 @@
    8.67      done
    8.68  qed
    8.69  
    8.70 -interpretation nat_dvd: dlat "op dvd :: [nat, nat] => bool"
    8.71 +interpretation nat_dvd!: dlat "op dvd :: [nat, nat] => bool"
    8.72    where "dlat.meet (op dvd) (x::nat) y = gcd x y"
    8.73      and "dlat.join (op dvd) (x::nat) y = lcm x y"
    8.74  proof -
    8.75 @@ -837,7 +837,7 @@
    8.76  
    8.77  subsubsection {* Interpretation of Functions *}
    8.78  
    8.79 -interpretation Dfun: Dmonoid "op o" "id :: 'a => 'a"
    8.80 +interpretation Dfun!: Dmonoid "op o" "id :: 'a => 'a"
    8.81    where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
    8.82  (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
    8.83  proof -
    8.84 @@ -887,7 +887,7 @@
    8.85    "(f :: unit => unit) = id"
    8.86    by rule simp
    8.87  
    8.88 -interpretation Dfun: Dgrp "op o" "id :: unit => unit"
    8.89 +interpretation Dfun!: Dgrp "op o" "id :: unit => unit"
    8.90    where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
    8.91  proof -
    8.92    have "Dmonoid op o (id :: 'a => 'a)" ..