--- a/src/HOL/HOLCF/Deflation.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/HOLCF/Deflation.thy Sun Mar 11 13:54:08 2012 +0100
@@ -379,9 +379,9 @@
by simp
qed
-locale pcpo_ep_pair = ep_pair +
- constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
- constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
+locale pcpo_ep_pair = ep_pair e p
+ for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
+ and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
begin
lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
--- a/src/HOL/HOLCF/Universal.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/HOLCF/Universal.thy Sun Mar 11 13:54:08 2012 +0100
@@ -291,8 +291,8 @@
text {* We use a locale to parameterize the construction over a chain
of approx functions on the type to be embedded. *}
-locale bifinite_approx_chain = approx_chain +
- constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
+locale bifinite_approx_chain =
+ approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
begin
subsubsection {* Choosing a maximal element from a finite set *}
--- a/src/HOL/Library/Numeral_Type.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Sun Mar 11 13:54:08 2012 +0100
@@ -135,8 +135,8 @@
end
-locale mod_ring = mod_type +
- constrains n :: int
+locale mod_ring = mod_type n Rep Abs
+ for n :: int
and Rep :: "'a::{number_ring} \<Rightarrow> int"
and Abs :: "int \<Rightarrow> 'a::{number_ring}"
begin
--- a/src/HOL/RealVector.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/RealVector.thy Sun Mar 11 13:54:08 2012 +0100
@@ -954,8 +954,7 @@
subsection {* Bounded Linear and Bilinear Operators *}
-locale bounded_linear = additive +
- constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
begin