prefer symbols;
authorwenzelm
Sat Oct 10 19:22:05 2015 +0200 (2015-10-10)
changeset 613849f5145281888
parent 61383 6762c8445138
child 61385 538100cc4399
prefer symbols;
NEWS
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/FinFun_Syntax.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Omega_Words_Fun.thy
src/HOL/Library/Preorder.thy
src/HOL/Metis_Examples/Abstraction.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/ex/Tarski.thy
     1.1 --- a/NEWS	Sat Oct 10 16:40:43 2015 +0200
     1.2 +++ b/NEWS	Sat Oct 10 19:22:05 2015 +0200
     1.3 @@ -251,6 +251,16 @@
     1.4    type_notation Map.map  (infixr "~=>" 0)
     1.5    notation Map.map_comp  (infixl "o'_m" 55)
     1.6  
     1.7 +  type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
     1.8 +
     1.9 +  notation FuncSet.funcset  (infixr "->" 60)
    1.10 +  notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)
    1.11 +
    1.12 +  notation Omega_Words_Fun.conc (infixr "conc" 65)
    1.13 +
    1.14 +  notation Preorder.equiv ("op ~~")
    1.15 +    and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
    1.16 +
    1.17  * The alternative notation "\<Colon>" for type and sort constraints has been
    1.18  removed: in LaTeX document output it looks the same as "::".
    1.19  INCOMPATIBILITY, use plain "::" instead.
     2.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:40:43 2015 +0200
     2.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 19:22:05 2015 +0200
     2.3 @@ -315,7 +315,7 @@
     2.4  context comm_monoid begin
     2.5  
     2.6  lemma finprod_insert [simp]:
     2.7 -  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
     2.8 +  "[| finite F; a \<notin> F; f \<in> F \<rightarrow> carrier G; f a \<in> carrier G |] ==>
     2.9     finprod G f (insert a F) = f a \<otimes> finprod G f F"
    2.10    apply (rule trans)
    2.11     apply (simp add: finprod_def)
    2.12 @@ -337,13 +337,13 @@
    2.13    case empty show ?case by simp
    2.14  next
    2.15    case (insert a A)
    2.16 -  have "(%i. \<one>) \<in> A -> carrier G" by auto
    2.17 +  have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
    2.18    with insert show ?case by simp
    2.19  qed simp
    2.20  
    2.21  lemma finprod_closed [simp]:
    2.22    fixes A
    2.23 -  assumes f: "f \<in> A -> carrier G" 
    2.24 +  assumes f: "f \<in> A \<rightarrow> carrier G" 
    2.25    shows "finprod G f A \<in> carrier G"
    2.26  using f
    2.27  proof (induct A rule: infinite_finite_induct)
    2.28 @@ -351,20 +351,20 @@
    2.29  next
    2.30    case (insert a A)
    2.31    then have a: "f a \<in> carrier G" by fast
    2.32 -  from insert have A: "f \<in> A -> carrier G" by fast
    2.33 +  from insert have A: "f \<in> A \<rightarrow> carrier G" by fast
    2.34    from insert A a show ?case by simp
    2.35  qed simp
    2.36  
    2.37  lemma funcset_Int_left [simp, intro]:
    2.38 -  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
    2.39 +  "[| f \<in> A \<rightarrow> C; f \<in> B \<rightarrow> C |] ==> f \<in> A Int B \<rightarrow> C"
    2.40    by fast
    2.41  
    2.42  lemma funcset_Un_left [iff]:
    2.43 -  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
    2.44 +  "(f \<in> A Un B \<rightarrow> C) = (f \<in> A \<rightarrow> C & f \<in> B \<rightarrow> C)"
    2.45    by fast
    2.46  
    2.47  lemma finprod_Un_Int:
    2.48 -  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
    2.49 +  "[| finite A; finite B; g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |] ==>
    2.50       finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
    2.51       finprod G g A \<otimes> finprod G g B"
    2.52  -- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
    2.53 @@ -373,46 +373,46 @@
    2.54  next
    2.55    case (insert a A)
    2.56    then have a: "g a \<in> carrier G" by fast
    2.57 -  from insert have A: "g \<in> A -> carrier G" by fast
    2.58 +  from insert have A: "g \<in> A \<rightarrow> carrier G" by fast
    2.59    from insert A a show ?case
    2.60      by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) 
    2.61  qed
    2.62  
    2.63  lemma finprod_Un_disjoint:
    2.64    "[| finite A; finite B; A Int B = {};
    2.65 -      g \<in> A -> carrier G; g \<in> B -> carrier G |]
    2.66 +      g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |]
    2.67     ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
    2.68    apply (subst finprod_Un_Int [symmetric])
    2.69        apply auto
    2.70    done
    2.71  
    2.72  lemma finprod_multf:
    2.73 -  "[| f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
    2.74 +  "[| f \<in> A \<rightarrow> carrier G; g \<in> A \<rightarrow> carrier G |] ==>
    2.75     finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
    2.76  proof (induct A rule: infinite_finite_induct)
    2.77    case empty show ?case by simp
    2.78  next
    2.79    case (insert a A) then
    2.80 -  have fA: "f \<in> A -> carrier G" by fast
    2.81 +  have fA: "f \<in> A \<rightarrow> carrier G" by fast
    2.82    from insert have fa: "f a \<in> carrier G" by fast
    2.83 -  from insert have gA: "g \<in> A -> carrier G" by fast
    2.84 +  from insert have gA: "g \<in> A \<rightarrow> carrier G" by fast
    2.85    from insert have ga: "g a \<in> carrier G" by fast
    2.86 -  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
    2.87 +  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A \<rightarrow> carrier G"
    2.88      by (simp add: Pi_def)
    2.89    show ?case
    2.90      by (simp add: insert fA fa gA ga fgA m_ac)
    2.91  qed simp
    2.92  
    2.93  lemma finprod_cong':
    2.94 -  "[| A = B; g \<in> B -> carrier G;
    2.95 +  "[| A = B; g \<in> B \<rightarrow> carrier G;
    2.96        !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
    2.97  proof -
    2.98 -  assume prems: "A = B" "g \<in> B -> carrier G"
    2.99 +  assume prems: "A = B" "g \<in> B \<rightarrow> carrier G"
   2.100      "!!i. i \<in> B ==> f i = g i"
   2.101    show ?thesis
   2.102    proof (cases "finite B")
   2.103      case True
   2.104 -    then have "!!A. [| A = B; g \<in> B -> carrier G;
   2.105 +    then have "!!A. [| A = B; g \<in> B \<rightarrow> carrier G;
   2.106        !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   2.107      proof induct
   2.108        case empty thus ?case by simp
   2.109 @@ -427,7 +427,7 @@
   2.110        next
   2.111          assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   2.112            "g \<in> insert x B \<rightarrow> carrier G"
   2.113 -        thus "f \<in> B -> carrier G" by fastforce
   2.114 +        thus "f \<in> B \<rightarrow> carrier G" by fastforce
   2.115        next
   2.116          assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
   2.117            "g \<in> insert x B \<rightarrow> carrier G"
   2.118 @@ -445,13 +445,13 @@
   2.119  qed
   2.120  
   2.121  lemma finprod_cong:
   2.122 -  "[| A = B; f \<in> B -> carrier G = True;
   2.123 +  "[| A = B; f \<in> B \<rightarrow> carrier G = True;
   2.124        !!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
   2.125    (* This order of prems is slightly faster (3%) than the last two swapped. *)
   2.126    by (rule finprod_cong') (auto simp add: simp_implies_def)
   2.127  
   2.128  text \<open>Usually, if this rule causes a failed congruence proof error,
   2.129 -  the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
   2.130 +  the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
   2.131    Adding @{thm [source] Pi_def} to the simpset is often useful.
   2.132    For this reason, @{thm [source] finprod_cong}
   2.133    is not added to the simpset by default.
   2.134 @@ -465,16 +465,16 @@
   2.135  context comm_monoid begin
   2.136  
   2.137  lemma finprod_0 [simp]:
   2.138 -  "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
   2.139 +  "f \<in> {0::nat} \<rightarrow> carrier G ==> finprod G f {..0} = f 0"
   2.140  by (simp add: Pi_def)
   2.141  
   2.142  lemma finprod_Suc [simp]:
   2.143 -  "f \<in> {..Suc n} -> carrier G ==>
   2.144 +  "f \<in> {..Suc n} \<rightarrow> carrier G ==>
   2.145     finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
   2.146  by (simp add: Pi_def atMost_Suc)
   2.147  
   2.148  lemma finprod_Suc2:
   2.149 -  "f \<in> {..Suc n} -> carrier G ==>
   2.150 +  "f \<in> {..Suc n} \<rightarrow> carrier G ==>
   2.151     finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
   2.152  proof (induct n)
   2.153    case 0 thus ?case by (simp add: Pi_def)
   2.154 @@ -483,7 +483,7 @@
   2.155  qed
   2.156  
   2.157  lemma finprod_mult [simp]:
   2.158 -  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
   2.159 +  "[| f \<in> {..n} \<rightarrow> carrier G; g \<in> {..n} \<rightarrow> carrier G |] ==>
   2.160       finprod G (%i. f i \<otimes> g i) {..n::nat} =
   2.161       finprod G f {..n} \<otimes> finprod G g {..n}"
   2.162    by (induct n) (simp_all add: m_ac Pi_def)
     3.1 --- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:40:43 2015 +0200
     3.2 +++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 19:22:05 2015 +0200
     3.3 @@ -576,7 +576,7 @@
     3.4  definition
     3.5    hom :: "_ => _ => ('a => 'b) set" where
     3.6    "hom G H =
     3.7 -    {h. h \<in> carrier G -> carrier H &
     3.8 +    {h. h \<in> carrier G \<rightarrow> carrier H &
     3.9        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
    3.10  
    3.11  lemma (in group) hom_compose:
     4.1 --- a/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:40:43 2015 +0200
     4.2 +++ b/src/HOL/Algebra/Ring.thy	Sat Oct 10 19:22:05 2015 +0200
     4.3 @@ -141,7 +141,7 @@
     4.4  
     4.5  lemmas finsum_cong = add.finprod_cong
     4.6  text \<open>Usually, if this rule causes a failed congruence proof error,
     4.7 -   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
     4.8 +   the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
     4.9     Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
    4.10  
    4.11  lemmas finsum_reindex = add.finprod_reindex
    4.12 @@ -490,7 +490,7 @@
    4.13  subsubsection \<open>Sums over Finite Sets\<close>
    4.14  
    4.15  lemma (in semiring) finsum_ldistr:
    4.16 -  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    4.17 +  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    4.18     finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
    4.19  proof (induct set: finite)
    4.20    case empty then show ?case by simp
    4.21 @@ -499,7 +499,7 @@
    4.22  qed
    4.23  
    4.24  lemma (in semiring) finsum_rdistr:
    4.25 -  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
    4.26 +  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    4.27     a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
    4.28  proof (induct set: finite)
    4.29    case empty then show ?case by simp
    4.30 @@ -609,7 +609,7 @@
    4.31  definition
    4.32    ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
    4.33    where "ring_hom R S =
    4.34 -    {h. h \<in> carrier R -> carrier S &
    4.35 +    {h. h \<in> carrier R \<rightarrow> carrier S &
    4.36        (ALL x y. x \<in> carrier R & y \<in> carrier R -->
    4.37          h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
    4.38        h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
    4.39 @@ -675,12 +675,12 @@
    4.40  qed
    4.41  
    4.42  lemma (in ring_hom_cring) hom_finsum [simp]:
    4.43 -  "f \<in> A -> carrier R ==>
    4.44 +  "f \<in> A \<rightarrow> carrier R ==>
    4.45    h (finsum R f A) = finsum S (h o f) A"
    4.46    by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
    4.47  
    4.48  lemma (in ring_hom_cring) hom_finprod:
    4.49 -  "f \<in> A -> carrier R ==>
    4.50 +  "f \<in> A \<rightarrow> carrier R ==>
    4.51    h (finprod R f A) = finprod S (h o f) A"
    4.52    by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
    4.53  
     5.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:40:43 2015 +0200
     5.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 19:22:05 2015 +0200
     5.3 @@ -54,7 +54,7 @@
     5.4  
     5.5  definition
     5.6    up :: "('a, 'm) ring_scheme => (nat => 'a) set"
     5.7 -  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
     5.8 +  where "up R = {f. f \<in> UNIV \<rightarrow> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
     5.9  
    5.10  definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
    5.11    where "UP R = \<lparr>
    5.12 @@ -309,8 +309,8 @@
    5.13    fix n
    5.14    {
    5.15      fix k and a b c :: "nat=>'a"
    5.16 -    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
    5.17 -      "c \<in> UNIV -> carrier R"
    5.18 +    assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
    5.19 +      "c \<in> UNIV \<rightarrow> carrier R"
    5.20      then have "k <= n ==>
    5.21        (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
    5.22        (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
    5.23 @@ -409,7 +409,7 @@
    5.24    fix n
    5.25    {
    5.26      fix k and a b :: "nat=>'a"
    5.27 -    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
    5.28 +    assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
    5.29      then have "k <= n ==>
    5.30        (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
    5.31        (is "_ \<Longrightarrow> ?eq k")
    5.32 @@ -956,7 +956,7 @@
    5.33  
    5.34  lemma coeff_finsum:
    5.35    assumes fin: "finite A"
    5.36 -  shows "p \<in> A -> carrier P ==>
    5.37 +  shows "p \<in> A \<rightarrow> carrier P ==>
    5.38      coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
    5.39    using fin by induct (auto simp: Pi_def)
    5.40  
    5.41 @@ -1095,11 +1095,11 @@
    5.42  begin
    5.43  
    5.44  theorem diagonal_sum:
    5.45 -  "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
    5.46 +  "[| f \<in> {..n + m::nat} \<rightarrow> carrier R; g \<in> {..n + m} \<rightarrow> carrier R |] ==>
    5.47    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
    5.48    (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
    5.49  proof -
    5.50 -  assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
    5.51 +  assume Rf: "f \<in> {..n + m} \<rightarrow> carrier R" and Rg: "g \<in> {..n + m} \<rightarrow> carrier R"
    5.52    {
    5.53      fix j
    5.54      have "j <= n + m ==>
    5.55 @@ -1129,7 +1129,7 @@
    5.56  
    5.57  theorem cauchy_product:
    5.58    assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
    5.59 -    and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
    5.60 +    and Rf: "f \<in> {..n} \<rightarrow> carrier R" and Rg: "g \<in> {..m} \<rightarrow> carrier R"
    5.61    shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
    5.62      (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"      (* State reverse direction? *)
    5.63  proof -
    5.64 @@ -1208,7 +1208,7 @@
    5.65    maybe it is not that necessary.\<close>
    5.66  
    5.67  lemma (in ring_hom_ring) hom_finsum [simp]:
    5.68 -  "f \<in> A -> carrier R ==>
    5.69 +  "f \<in> A \<rightarrow> carrier R ==>
    5.70    h (finsum R f A) = finsum S (h o f) A"
    5.71    by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
    5.72  
     6.1 --- a/src/HOL/Library/Extended_Nat.thy	Sat Oct 10 16:40:43 2015 +0200
     6.2 +++ b/src/HOL/Library/Extended_Nat.thy	Sat Oct 10 19:22:05 2015 +0200
     6.3 @@ -10,10 +10,7 @@
     6.4  begin
     6.5  
     6.6  class infinity =
     6.7 -  fixes infinity :: "'a"
     6.8 -
     6.9 -notation (xsymbols)
    6.10 -  infinity  ("\<infinity>")
    6.11 +  fixes infinity :: "'a"  ("\<infinity>")
    6.12  
    6.13  
    6.14  subsection \<open>Type definition\<close>
     7.1 --- a/src/HOL/Library/FinFun.thy	Sat Oct 10 16:40:43 2015 +0200
     7.2 +++ b/src/HOL/Library/FinFun.thy	Sat Oct 10 19:22:05 2015 +0200
     7.3 @@ -76,7 +76,7 @@
     7.4  
     7.5  definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
     7.6  
     7.7 -typedef ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
     7.8 +typedef ('a,'b) finfun  ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
     7.9    morphisms finfun_apply Abs_finfun
    7.10  proof -
    7.11    have "\<exists>f. finite {x. f x \<noteq> undefined}"
    7.12 @@ -1528,9 +1528,6 @@
    7.13  text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
    7.14  
    7.15  no_type_notation
    7.16 -  finfun ("(_ =>f /_)" [22, 21] 21)
    7.17 -
    7.18 -no_type_notation (xsymbols)
    7.19    finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    7.20  
    7.21  no_notation
     8.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Sat Oct 10 16:40:43 2015 +0200
     8.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Sat Oct 10 19:22:05 2015 +0200
     8.3 @@ -7,9 +7,6 @@
     8.4  begin
     8.5  
     8.6  type_notation
     8.7 -  finfun ("(_ =>f /_)" [22, 21] 21)
     8.8 -
     8.9 -type_notation (xsymbols)
    8.10    finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
    8.11  
    8.12  notation
     9.1 --- a/src/HOL/Library/FuncSet.thy	Sat Oct 10 16:40:43 2015 +0200
     9.2 +++ b/src/HOL/Library/FuncSet.thy	Sat Oct 10 19:22:05 2015 +0200
     9.3 @@ -17,11 +17,8 @@
     9.4  definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
     9.5    where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
     9.6  
     9.7 -abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "->" 60)
     9.8 -  where "A -> B \<equiv> Pi A (\<lambda>_. B)"
     9.9 -
    9.10 -notation (xsymbols)
    9.11 -  funcset  (infixr "\<rightarrow>" 60)
    9.12 +abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
    9.13 +  where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
    9.14  
    9.15  syntax
    9.16    "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
    9.17 @@ -356,11 +353,8 @@
    9.18    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
    9.19  translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
    9.20  
    9.21 -abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
    9.22 -  where "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
    9.23 -
    9.24 -notation (xsymbols)
    9.25 -  extensional_funcset  (infixr "\<rightarrow>\<^sub>E" 60)
    9.26 +abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
    9.27 +  where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
    9.28  
    9.29  lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
    9.30    by (simp add: PiE_def)
    10.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 16:40:43 2015 +0200
    10.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 19:22:05 2015 +0200
    10.3 @@ -44,17 +44,13 @@
    10.4  \<close>
    10.5  
    10.6  definition
    10.7 -  conc :: "['a list, 'a word] \<Rightarrow> 'a word"    (infixr "conc" 65)
    10.8 -  where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"
    10.9 +  conc :: "['a list, 'a word] \<Rightarrow> 'a word"  (infixr "\<frown>" 65)
   10.10 +  where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
   10.11  
   10.12  definition
   10.13 -  iter :: "'a list \<Rightarrow> 'a word"
   10.14 +  iter :: "'a list \<Rightarrow> 'a word"  ("(_\<^sup>\<omega>)" [1000])
   10.15    where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
   10.16  
   10.17 -notation (xsymbols)
   10.18 -  conc (infixr "\<frown>" 65) and
   10.19 -  iter ("(_\<^sup>\<omega>)" [1000])
   10.20 -
   10.21  lemma conc_empty[simp]: "[] \<frown> w = w"
   10.22    unfolding conc_def by auto
   10.23  
    11.1 --- a/src/HOL/Library/Preorder.thy	Sat Oct 10 16:40:43 2015 +0200
    11.2 +++ b/src/HOL/Library/Preorder.thy	Sat Oct 10 19:22:05 2015 +0200
    11.3 @@ -13,10 +13,6 @@
    11.4    "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
    11.5  
    11.6  notation
    11.7 -  equiv ("op ~~") and
    11.8 -  equiv ("(_/ ~~ _)" [51, 51] 50)
    11.9 -  
   11.10 -notation (xsymbols)
   11.11    equiv ("op \<approx>") and
   11.12    equiv ("(_/ \<approx> _)"  [51, 51] 50)
   11.13  
    12.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Sat Oct 10 16:40:43 2015 +0200
    12.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Sat Oct 10 19:22:05 2015 +0200
    12.3 @@ -142,8 +142,8 @@
    12.4  by auto
    12.5  
    12.6  lemma
    12.7 -  "map (\<lambda>w. (w -> w, w \<times> w)) xs =
    12.8 -   zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
    12.9 +  "map (\<lambda>w. (w \<rightarrow> w, w \<times> w)) xs =
   12.10 +   zip (map (\<lambda>w. w \<rightarrow> w) xs) (map (\<lambda>w. w \<times> w) xs)"
   12.11  apply (induct xs)
   12.12   apply (metis list.map(1) zip_Nil)
   12.13  by auto
    13.1 --- a/src/HOL/Metis_Examples/Tarski.thy	Sat Oct 10 16:40:43 2015 +0200
    13.2 +++ b/src/HOL/Metis_Examples/Tarski.thy	Sat Oct 10 19:22:05 2015 +0200
    13.3 @@ -97,7 +97,7 @@
    13.4  
    13.5  definition CLF_set :: "('a potype * ('a => 'a)) set" where
    13.6    "CLF_set = (SIGMA cl: CompleteLattice.
    13.7 -            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
    13.8 +            {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
    13.9  
   13.10  locale CLF = CL +
   13.11    fixes f :: "'a => 'a"
   13.12 @@ -402,7 +402,7 @@
   13.13  declare (in CLF) f_cl [simp]
   13.14  
   13.15  lemma (in CLF) [simp]:
   13.16 -    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
   13.17 +    "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
   13.18  proof -
   13.19    have "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> {R \<in> pset v \<rightarrow> pset v. monotone R (pset v) (order v)}"
   13.20      unfolding CLF_set_def using SigmaE2 by blast
   13.21 @@ -415,7 +415,7 @@
   13.22      using F1 by metis
   13.23  qed
   13.24  
   13.25 -lemma (in CLF) f_in_funcset: "f \<in> A -> A"
   13.26 +lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
   13.27  by (simp add: A_def)
   13.28  
   13.29  lemma (in CLF) monotone_f: "monotone f A r"
   13.30 @@ -904,7 +904,7 @@
   13.31  done
   13.32  
   13.33  
   13.34 -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
   13.35 +lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 \<rightarrow> intY1"
   13.36  apply (rule restrict_in_funcset)
   13.37  apply (metis intY1_f_closed restrict_in_funcset)
   13.38  done
    14.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Sat Oct 10 16:40:43 2015 +0200
    14.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Sat Oct 10 19:22:05 2015 +0200
    14.3 @@ -1697,7 +1697,7 @@
    14.4  subsubsection {* Measurable functions *}
    14.5  
    14.6  definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
    14.7 -  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
    14.8 +  "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
    14.9  
   14.10  lemma measurableI:
   14.11    "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
    15.1 --- a/src/HOL/ex/Tarski.thy	Sat Oct 10 16:40:43 2015 +0200
    15.2 +++ b/src/HOL/ex/Tarski.thy	Sat Oct 10 19:22:05 2015 +0200
    15.3 @@ -84,7 +84,7 @@
    15.4  definition
    15.5    CLF_set :: "('a potype * ('a => 'a)) set" where
    15.6    "CLF_set = (SIGMA cl: CompleteLattice.
    15.7 -            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
    15.8 +            {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
    15.9  
   15.10  definition
   15.11    induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where
   15.12 @@ -445,7 +445,7 @@
   15.13  \<close>
   15.14  
   15.15  lemma (in CLF) [simp]:
   15.16 -    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
   15.17 +    "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
   15.18  apply (insert f_cl)
   15.19  apply (simp add: CLF_set_def)
   15.20  done
   15.21 @@ -453,7 +453,7 @@
   15.22  declare (in CLF) f_cl [simp]
   15.23  
   15.24  
   15.25 -lemma (in CLF) f_in_funcset: "f \<in> A -> A"
   15.26 +lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
   15.27  by (simp add: A_def)
   15.28  
   15.29  lemma (in CLF) monotone_f: "monotone f A r"