--- a/NEWS Sat Oct 10 16:40:43 2015 +0200
+++ b/NEWS Sat Oct 10 19:22:05 2015 +0200
@@ -251,6 +251,16 @@
type_notation Map.map (infixr "~=>" 0)
notation Map.map_comp (infixl "o'_m" 55)
+ type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
+
+ notation FuncSet.funcset (infixr "->" 60)
+ notation FuncSet.extensional_funcset (infixr "->\<^sub>E" 60)
+
+ notation Omega_Words_Fun.conc (infixr "conc" 65)
+
+ notation Preorder.equiv ("op ~~")
+ and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
+
* The alternative notation "\<Colon>" for type and sort constraints has been
removed: in LaTeX document output it looks the same as "::".
INCOMPATIBILITY, use plain "::" instead.
--- a/src/HOL/Algebra/FiniteProduct.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy Sat Oct 10 19:22:05 2015 +0200
@@ -315,7 +315,7 @@
context comm_monoid begin
lemma finprod_insert [simp]:
- "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
+ "[| finite F; a \<notin> F; f \<in> F \<rightarrow> carrier G; f a \<in> carrier G |] ==>
finprod G f (insert a F) = f a \<otimes> finprod G f F"
apply (rule trans)
apply (simp add: finprod_def)
@@ -337,13 +337,13 @@
case empty show ?case by simp
next
case (insert a A)
- have "(%i. \<one>) \<in> A -> carrier G" by auto
+ have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
with insert show ?case by simp
qed simp
lemma finprod_closed [simp]:
fixes A
- assumes f: "f \<in> A -> carrier G"
+ assumes f: "f \<in> A \<rightarrow> carrier G"
shows "finprod G f A \<in> carrier G"
using f
proof (induct A rule: infinite_finite_induct)
@@ -351,20 +351,20 @@
next
case (insert a A)
then have a: "f a \<in> carrier G" by fast
- from insert have A: "f \<in> A -> carrier G" by fast
+ from insert have A: "f \<in> A \<rightarrow> carrier G" by fast
from insert A a show ?case by simp
qed simp
lemma funcset_Int_left [simp, intro]:
- "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
+ "[| f \<in> A \<rightarrow> C; f \<in> B \<rightarrow> C |] ==> f \<in> A Int B \<rightarrow> C"
by fast
lemma funcset_Un_left [iff]:
- "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
+ "(f \<in> A Un B \<rightarrow> C) = (f \<in> A \<rightarrow> C & f \<in> B \<rightarrow> C)"
by fast
lemma finprod_Un_Int:
- "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+ "[| finite A; finite B; g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |] ==>
finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
finprod G g A \<otimes> finprod G g B"
-- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
@@ -373,46 +373,46 @@
next
case (insert a A)
then have a: "g a \<in> carrier G" by fast
- from insert have A: "g \<in> A -> carrier G" by fast
+ from insert have A: "g \<in> A \<rightarrow> carrier G" by fast
from insert A a show ?case
by (simp add: m_ac Int_insert_left insert_absorb Int_mono2)
qed
lemma finprod_Un_disjoint:
"[| finite A; finite B; A Int B = {};
- g \<in> A -> carrier G; g \<in> B -> carrier G |]
+ g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |]
==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
apply (subst finprod_Un_Int [symmetric])
apply auto
done
lemma finprod_multf:
- "[| f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+ "[| f \<in> A \<rightarrow> carrier G; g \<in> A \<rightarrow> carrier G |] ==>
finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
proof (induct A rule: infinite_finite_induct)
case empty show ?case by simp
next
case (insert a A) then
- have fA: "f \<in> A -> carrier G" by fast
+ have fA: "f \<in> A \<rightarrow> carrier G" by fast
from insert have fa: "f a \<in> carrier G" by fast
- from insert have gA: "g \<in> A -> carrier G" by fast
+ from insert have gA: "g \<in> A \<rightarrow> carrier G" by fast
from insert have ga: "g a \<in> carrier G" by fast
- from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
+ from insert have fgA: "(%x. f x \<otimes> g x) \<in> A \<rightarrow> carrier G"
by (simp add: Pi_def)
show ?case
by (simp add: insert fA fa gA ga fgA m_ac)
qed simp
lemma finprod_cong':
- "[| A = B; g \<in> B -> carrier G;
+ "[| A = B; g \<in> B \<rightarrow> carrier G;
!!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
proof -
- assume prems: "A = B" "g \<in> B -> carrier G"
+ assume prems: "A = B" "g \<in> B \<rightarrow> carrier G"
"!!i. i \<in> B ==> f i = g i"
show ?thesis
proof (cases "finite B")
case True
- then have "!!A. [| A = B; g \<in> B -> carrier G;
+ then have "!!A. [| A = B; g \<in> B \<rightarrow> carrier G;
!!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
proof induct
case empty thus ?case by simp
@@ -427,7 +427,7 @@
next
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
- thus "f \<in> B -> carrier G" by fastforce
+ thus "f \<in> B \<rightarrow> carrier G" by fastforce
next
assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
"g \<in> insert x B \<rightarrow> carrier G"
@@ -445,13 +445,13 @@
qed
lemma finprod_cong:
- "[| A = B; f \<in> B -> carrier G = True;
+ "[| A = B; f \<in> B \<rightarrow> carrier G = True;
!!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
(* This order of prems is slightly faster (3%) than the last two swapped. *)
by (rule finprod_cong') (auto simp add: simp_implies_def)
text \<open>Usually, if this rule causes a failed congruence proof error,
- the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+ the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.
For this reason, @{thm [source] finprod_cong}
is not added to the simpset by default.
@@ -465,16 +465,16 @@
context comm_monoid begin
lemma finprod_0 [simp]:
- "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
+ "f \<in> {0::nat} \<rightarrow> carrier G ==> finprod G f {..0} = f 0"
by (simp add: Pi_def)
lemma finprod_Suc [simp]:
- "f \<in> {..Suc n} -> carrier G ==>
+ "f \<in> {..Suc n} \<rightarrow> carrier G ==>
finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
by (simp add: Pi_def atMost_Suc)
lemma finprod_Suc2:
- "f \<in> {..Suc n} -> carrier G ==>
+ "f \<in> {..Suc n} \<rightarrow> carrier G ==>
finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
proof (induct n)
case 0 thus ?case by (simp add: Pi_def)
@@ -483,7 +483,7 @@
qed
lemma finprod_mult [simp]:
- "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
+ "[| f \<in> {..n} \<rightarrow> carrier G; g \<in> {..n} \<rightarrow> carrier G |] ==>
finprod G (%i. f i \<otimes> g i) {..n::nat} =
finprod G f {..n} \<otimes> finprod G g {..n}"
by (induct n) (simp_all add: m_ac Pi_def)
--- a/src/HOL/Algebra/Group.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/Group.thy Sat Oct 10 19:22:05 2015 +0200
@@ -576,7 +576,7 @@
definition
hom :: "_ => _ => ('a => 'b) set" where
"hom G H =
- {h. h \<in> carrier G -> carrier H &
+ {h. h \<in> carrier G \<rightarrow> carrier H &
(\<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)}"
lemma (in group) hom_compose:
--- a/src/HOL/Algebra/Ring.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy Sat Oct 10 19:22:05 2015 +0200
@@ -141,7 +141,7 @@
lemmas finsum_cong = add.finprod_cong
text \<open>Usually, if this rule causes a failed congruence proof error,
- the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+ the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
lemmas finsum_reindex = add.finprod_reindex
@@ -490,7 +490,7 @@
subsubsection \<open>Sums over Finite Sets\<close>
lemma (in semiring) finsum_ldistr:
- "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+ "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
proof (induct set: finite)
case empty then show ?case by simp
@@ -499,7 +499,7 @@
qed
lemma (in semiring) finsum_rdistr:
- "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+ "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
proof (induct set: finite)
case empty then show ?case by simp
@@ -609,7 +609,7 @@
definition
ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
where "ring_hom R S =
- {h. h \<in> carrier R -> carrier S &
+ {h. h \<in> carrier R \<rightarrow> carrier S &
(ALL x y. x \<in> carrier R & y \<in> carrier R -->
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) &
h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
@@ -675,12 +675,12 @@
qed
lemma (in ring_hom_cring) hom_finsum [simp]:
- "f \<in> A -> carrier R ==>
+ "f \<in> A \<rightarrow> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
lemma (in ring_hom_cring) hom_finprod:
- "f \<in> A -> carrier R ==>
+ "f \<in> A \<rightarrow> carrier R ==>
h (finprod R f A) = finprod S (h o f) A"
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
--- a/src/HOL/Algebra/UnivPoly.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Sat Oct 10 19:22:05 2015 +0200
@@ -54,7 +54,7 @@
definition
up :: "('a, 'm) ring_scheme => (nat => 'a) set"
- where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+ where "up R = {f. f \<in> UNIV \<rightarrow> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
where "UP R = \<lparr>
@@ -309,8 +309,8 @@
fix n
{
fix k and a b c :: "nat=>'a"
- assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
- "c \<in> UNIV -> carrier R"
+ assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
+ "c \<in> UNIV \<rightarrow> carrier R"
then have "k <= n ==>
(\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
(\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
@@ -409,7 +409,7 @@
fix n
{
fix k and a b :: "nat=>'a"
- assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
+ assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
then have "k <= n ==>
(\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
(is "_ \<Longrightarrow> ?eq k")
@@ -956,7 +956,7 @@
lemma coeff_finsum:
assumes fin: "finite A"
- shows "p \<in> A -> carrier P ==>
+ shows "p \<in> A \<rightarrow> carrier P ==>
coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
using fin by induct (auto simp: Pi_def)
@@ -1095,11 +1095,11 @@
begin
theorem diagonal_sum:
- "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
+ "[| f \<in> {..n + m::nat} \<rightarrow> carrier R; g \<in> {..n + m} \<rightarrow> carrier R |] ==>
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
proof -
- assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
+ assume Rf: "f \<in> {..n + m} \<rightarrow> carrier R" and Rg: "g \<in> {..n + m} \<rightarrow> carrier R"
{
fix j
have "j <= n + m ==>
@@ -1129,7 +1129,7 @@
theorem cauchy_product:
assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
- and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
+ and Rf: "f \<in> {..n} \<rightarrow> carrier R" and Rg: "g \<in> {..m} \<rightarrow> carrier R"
shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
(\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)" (* State reverse direction? *)
proof -
@@ -1208,7 +1208,7 @@
maybe it is not that necessary.\<close>
lemma (in ring_hom_ring) hom_finsum [simp]:
- "f \<in> A -> carrier R ==>
+ "f \<in> A \<rightarrow> carrier R ==>
h (finsum R f A) = finsum S (h o f) A"
by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
--- a/src/HOL/Library/Extended_Nat.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Sat Oct 10 19:22:05 2015 +0200
@@ -10,10 +10,7 @@
begin
class infinity =
- fixes infinity :: "'a"
-
-notation (xsymbols)
- infinity ("\<infinity>")
+ fixes infinity :: "'a" ("\<infinity>")
subsection \<open>Type definition\<close>
--- a/src/HOL/Library/FinFun.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FinFun.thy Sat Oct 10 19:22:05 2015 +0200
@@ -76,7 +76,7 @@
definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
-typedef ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
+typedef ('a,'b) finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
morphisms finfun_apply Abs_finfun
proof -
have "\<exists>f. finite {x. f x \<noteq> undefined}"
@@ -1528,9 +1528,6 @@
text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
no_type_notation
- finfun ("(_ =>f /_)" [22, 21] 21)
-
-no_type_notation (xsymbols)
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
no_notation
--- a/src/HOL/Library/FinFun_Syntax.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FinFun_Syntax.thy Sat Oct 10 19:22:05 2015 +0200
@@ -7,9 +7,6 @@
begin
type_notation
- finfun ("(_ =>f /_)" [22, 21] 21)
-
-type_notation (xsymbols)
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
notation
--- a/src/HOL/Library/FuncSet.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FuncSet.thy Sat Oct 10 19:22:05 2015 +0200
@@ -17,11 +17,8 @@
definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
-abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->" 60)
- where "A -> B \<equiv> Pi A (\<lambda>_. B)"
-
-notation (xsymbols)
- funcset (infixr "\<rightarrow>" 60)
+abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>" 60)
+ where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
syntax
"_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3PI _:_./ _)" 10)
@@ -356,11 +353,8 @@
"_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
-abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
- where "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
-
-notation (xsymbols)
- extensional_funcset (infixr "\<rightarrow>\<^sub>E" 60)
+abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
+ where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
by (simp add: PiE_def)
--- a/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Sat Oct 10 19:22:05 2015 +0200
@@ -44,17 +44,13 @@
\<close>
definition
- conc :: "['a list, 'a word] \<Rightarrow> 'a word" (infixr "conc" 65)
- where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"
+ conc :: "['a list, 'a word] \<Rightarrow> 'a word" (infixr "\<frown>" 65)
+ where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
definition
- iter :: "'a list \<Rightarrow> 'a word"
+ iter :: "'a list \<Rightarrow> 'a word" ("(_\<^sup>\<omega>)" [1000])
where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
-notation (xsymbols)
- conc (infixr "\<frown>" 65) and
- iter ("(_\<^sup>\<omega>)" [1000])
-
lemma conc_empty[simp]: "[] \<frown> w = w"
unfolding conc_def by auto
--- a/src/HOL/Library/Preorder.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Preorder.thy Sat Oct 10 19:22:05 2015 +0200
@@ -13,10 +13,6 @@
"equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
notation
- equiv ("op ~~") and
- equiv ("(_/ ~~ _)" [51, 51] 50)
-
-notation (xsymbols)
equiv ("op \<approx>") and
equiv ("(_/ \<approx> _)" [51, 51] 50)
--- a/src/HOL/Metis_Examples/Abstraction.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy Sat Oct 10 19:22:05 2015 +0200
@@ -142,8 +142,8 @@
by auto
lemma
- "map (\<lambda>w. (w -> w, w \<times> w)) xs =
- zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
+ "map (\<lambda>w. (w \<rightarrow> w, w \<times> w)) xs =
+ zip (map (\<lambda>w. w \<rightarrow> w) xs) (map (\<lambda>w. w \<times> w) xs)"
apply (induct xs)
apply (metis list.map(1) zip_Nil)
by auto
--- a/src/HOL/Metis_Examples/Tarski.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy Sat Oct 10 19:22:05 2015 +0200
@@ -97,7 +97,7 @@
definition CLF_set :: "('a potype * ('a => 'a)) set" where
"CLF_set = (SIGMA cl: CompleteLattice.
- {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
+ {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
locale CLF = CL +
fixes f :: "'a => 'a"
@@ -402,7 +402,7 @@
declare (in CLF) f_cl [simp]
lemma (in CLF) [simp]:
- "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
+ "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
proof -
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)}"
unfolding CLF_set_def using SigmaE2 by blast
@@ -415,7 +415,7 @@
using F1 by metis
qed
-lemma (in CLF) f_in_funcset: "f \<in> A -> A"
+lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
by (simp add: A_def)
lemma (in CLF) monotone_f: "monotone f A r"
@@ -904,7 +904,7 @@
done
-lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
+lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 \<rightarrow> intY1"
apply (rule restrict_in_funcset)
apply (metis intY1_f_closed restrict_in_funcset)
done
--- a/src/HOL/Probability/Sigma_Algebra.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Sat Oct 10 19:22:05 2015 +0200
@@ -1697,7 +1697,7 @@
subsubsection {* Measurable functions *}
definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
- "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
+ "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
lemma measurableI:
"(\<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>
--- a/src/HOL/ex/Tarski.thy Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/ex/Tarski.thy Sat Oct 10 19:22:05 2015 +0200
@@ -84,7 +84,7 @@
definition
CLF_set :: "('a potype * ('a => 'a)) set" where
"CLF_set = (SIGMA cl: CompleteLattice.
- {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
+ {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
definition
induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where
@@ -445,7 +445,7 @@
\<close>
lemma (in CLF) [simp]:
- "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
+ "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
apply (insert f_cl)
apply (simp add: CLF_set_def)
done
@@ -453,7 +453,7 @@
declare (in CLF) f_cl [simp]
-lemma (in CLF) f_in_funcset: "f \<in> A -> A"
+lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
by (simp add: A_def)
lemma (in CLF) monotone_f: "monotone f A r"