eliminated old-fashioned 'constrains' element;
authorwenzelm
Sun Mar 11 13:54:08 2012 +0100 (2012-03-11)
changeset 468686c250adbe101
parent 46867 0883804b67bb
child 46869 26a9a4e0a631
eliminated old-fashioned 'constrains' element;
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Universal.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 13:39:16 2012 +0100
     1.2 +++ b/src/HOL/HOLCF/Deflation.thy	Sun Mar 11 13:54:08 2012 +0100
     1.3 @@ -379,9 +379,9 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 -locale pcpo_ep_pair = ep_pair +
     1.8 -  constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
     1.9 -  constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.10 +locale pcpo_ep_pair = ep_pair e p
    1.11 +  for e :: "'a::pcpo \<rightarrow> 'b::pcpo"
    1.12 +  and p :: "'b::pcpo \<rightarrow> 'a::pcpo"
    1.13  begin
    1.14  
    1.15  lemma e_strict [simp]: "e\<cdot>\<bottom> = \<bottom>"
     2.1 --- a/src/HOL/HOLCF/Universal.thy	Sun Mar 11 13:39:16 2012 +0100
     2.2 +++ b/src/HOL/HOLCF/Universal.thy	Sun Mar 11 13:54:08 2012 +0100
     2.3 @@ -291,8 +291,8 @@
     2.4  text {* We use a locale to parameterize the construction over a chain
     2.5  of approx functions on the type to be embedded. *}
     2.6  
     2.7 -locale bifinite_approx_chain = approx_chain +
     2.8 -  constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
     2.9 +locale bifinite_approx_chain =
    2.10 +  approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
    2.11  begin
    2.12  
    2.13  subsubsection {* Choosing a maximal element from a finite set *}
     3.1 --- a/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 13:39:16 2012 +0100
     3.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sun Mar 11 13:54:08 2012 +0100
     3.3 @@ -135,8 +135,8 @@
     3.4  
     3.5  end
     3.6  
     3.7 -locale mod_ring = mod_type +
     3.8 -  constrains n :: int
     3.9 +locale mod_ring = mod_type n Rep Abs
    3.10 +  for n :: int
    3.11    and Rep :: "'a::{number_ring} \<Rightarrow> int"
    3.12    and Abs :: "int \<Rightarrow> 'a::{number_ring}"
    3.13  begin
     4.1 --- a/src/HOL/RealVector.thy	Sun Mar 11 13:39:16 2012 +0100
     4.2 +++ b/src/HOL/RealVector.thy	Sun Mar 11 13:54:08 2012 +0100
     4.3 @@ -954,8 +954,7 @@
     4.4  
     4.5  subsection {* Bounded Linear and Bilinear Operators *}
     4.6  
     4.7 -locale bounded_linear = additive +
     4.8 -  constrains f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
     4.9 +locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
    4.10    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
    4.11    assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    4.12  begin