# HG changeset patch
# User wenzelm
# Date 1331470448 -3600
# Node ID 6c250adbe101c83080ecf1bf5a311c7bdf98c014
# Parent  0883804b67bb9842e4125c1c6d5c1b8f15ddd374
eliminated old-fashioned 'constrains' element;

diff -r 0883804b67bb -r 6c250adbe101 src/HOL/HOLCF/Deflation.thy
--- 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>"
diff -r 0883804b67bb -r 6c250adbe101 src/HOL/HOLCF/Universal.thy
--- 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 *}
diff -r 0883804b67bb -r 6c250adbe101 src/HOL/Library/Numeral_Type.thy
--- 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
diff -r 0883804b67bb -r 6c250adbe101 src/HOL/RealVector.thy
--- 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