--- a/src/FOL/IFOL.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/IFOL.thy Thu Jan 03 21:15:52 2019 +0100
@@ -31,13 +31,13 @@
typedecl o
judgment
- Trueprop :: "o \<Rightarrow> prop" ("(_)" 5)
+ Trueprop :: "o \<Rightarrow> prop" (\<open>(_)\<close> 5)
subsubsection \<open>Equality\<close>
axiomatization
- eq :: "['a, 'a] \<Rightarrow> o" (infixl "=" 50)
+ eq :: "['a, 'a] \<Rightarrow> o" (infixl \<open>=\<close> 50)
where
refl: "a = a" and
subst: "a = b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
@@ -47,9 +47,9 @@
axiomatization
False :: o and
- conj :: "[o, o] => o" (infixr "\<and>" 35) and
- disj :: "[o, o] => o" (infixr "\<or>" 30) and
- imp :: "[o, o] => o" (infixr "\<longrightarrow>" 25)
+ conj :: "[o, o] => o" (infixr \<open>\<and>\<close> 35) and
+ disj :: "[o, o] => o" (infixr \<open>\<or>\<close> 30) and
+ imp :: "[o, o] => o" (infixr \<open>\<longrightarrow>\<close> 25)
where
conjI: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q" and
conjunct1: "P \<and> Q \<Longrightarrow> P" and
@@ -68,8 +68,8 @@
subsubsection \<open>Quantifiers\<close>
axiomatization
- All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<forall>" 10) and
- Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>" 10)
+ All :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<forall>\<close> 10) and
+ Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<exists>\<close> 10)
where
allI: "(\<And>x. P(x)) \<Longrightarrow> (\<forall>x. P(x))" and
spec: "(\<forall>x. P(x)) \<Longrightarrow> P(x)" and
@@ -81,35 +81,35 @@
definition "True \<equiv> False \<longrightarrow> False"
-definition Not ("\<not> _" [40] 40)
+definition Not (\<open>\<not> _\<close> [40] 40)
where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
-definition iff (infixr "\<longleftrightarrow>" 25)
+definition iff (infixr \<open>\<longleftrightarrow>\<close> 25)
where "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
-definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder "\<exists>!" 10)
+definition Ex1 :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<exists>!\<close> 10)
where ex1_def: "\<exists>!x. P(x) \<equiv> \<exists>x. P(x) \<and> (\<forall>y. P(y) \<longrightarrow> y = x)"
axiomatization where \<comment> \<open>Reflection, admissible\<close>
eq_reflection: "(x = y) \<Longrightarrow> (x \<equiv> y)" and
iff_reflection: "(P \<longleftrightarrow> Q) \<Longrightarrow> (P \<equiv> Q)"
-abbreviation not_equal :: "['a, 'a] \<Rightarrow> o" (infixl "\<noteq>" 50)
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> o" (infixl \<open>\<noteq>\<close> 50)
where "x \<noteq> y \<equiv> \<not> (x = y)"
subsubsection \<open>Old-style ASCII syntax\<close>
notation (ASCII)
- not_equal (infixl "~=" 50) and
- Not ("~ _" [40] 40) and
- conj (infixr "&" 35) and
- disj (infixr "|" 30) and
- All (binder "ALL " 10) and
- Ex (binder "EX " 10) and
- Ex1 (binder "EX! " 10) and
- imp (infixr "-->" 25) and
- iff (infixr "<->" 25)
+ not_equal (infixl \<open>~=\<close> 50) and
+ Not (\<open>~ _\<close> [40] 40) and
+ conj (infixr \<open>&\<close> 35) and
+ disj (infixr \<open>|\<close> 30) and
+ All (binder \<open>ALL \<close> 10) and
+ Ex (binder \<open>EX \<close> 10) and
+ Ex1 (binder \<open>EX! \<close> 10) and
+ imp (infixr \<open>-->\<close> 25) and
+ iff (infixr \<open><->\<close> 25)
subsection \<open>Lemmas and proof tools\<close>
@@ -764,10 +764,10 @@
where "Let(s, f) \<equiv> f(s)"
syntax
- "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
- "" :: "letbind => letbinds" ("_")
- "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+ "_bind" :: "[pttrn, 'a] => letbind" (\<open>(2_ =/ _)\<close> 10)
+ "" :: "letbind => letbinds" (\<open>_\<close>)
+ "_binds" :: "[letbind, letbinds] => letbinds" (\<open>_;/ _\<close>)
+ "_Let" :: "[letbinds, 'a] => 'a" (\<open>(let (_)/ in (_))\<close> 10)
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Jan 03 21:15:52 2019 +0100
@@ -11,9 +11,9 @@
typedecl int
instance int :: "term" ..
-consts plus :: "int => int => int" (infixl "+" 60)
- zero :: int ("0")
- minus :: "int => int" ("- _")
+consts plus :: "int => int => int" (infixl \<open>+\<close> 60)
+ zero :: int (\<open>0\<close>)
+ minus :: "int => int" (\<open>- _\<close>)
axiomatization where
int_assoc: "(x + y::int) + z = x + (y + z)" and
@@ -34,17 +34,17 @@
Fails, cannot generalise parameter.
*)
-locale param3 = fixes p (infix ".." 50)
+locale param3 = fixes p (infix \<open>..\<close> 50)
print_locale! param3
-locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
+locale param4 = fixes p :: "'a => 'a => 'a" (infix \<open>..\<close> 50)
print_locale! param4
subsection \<open>Incremental type constraints\<close>
locale constraint1 =
- fixes prod (infixl "**" 65)
+ fixes prod (infixl \<open>**\<close> 65)
assumes l_id: "x ** y = x"
assumes assoc: "(x ** y) ** z = x ** (y ** z)"
print_locale! constraint1
@@ -58,7 +58,7 @@
section \<open>Inheritance\<close>
locale semi =
- fixes prod (infixl "**" 65)
+ fixes prod (infixl \<open>**\<close> 65)
assumes assoc: "(x ** y) ** z = x ** (y ** z)"
print_locale! semi thm semi_def
@@ -68,13 +68,13 @@
and linv: "inv(x) ** x = one"
print_locale! lgrp thm lgrp_def lgrp_axioms_def
-locale add_lgrp = semi "(++)" for sum (infixl "++" 60) +
+locale add_lgrp = semi "(++)" for sum (infixl \<open>++\<close> 60) +
fixes zero and neg
assumes lzero: "zero ++ x = x"
and lneg: "neg(x) ++ x = zero"
print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
-locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
+locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl \<open>++\<close> 60)
print_locale! rev_lgrp thm rev_lgrp_def
locale hom = f: semi f + g: semi g for f and g
@@ -94,13 +94,13 @@
section \<open>Syntax declarations\<close>
locale logic =
- fixes land (infixl "&&" 55)
- and lnot ("-- _" [60] 60)
+ fixes land (infixl \<open>&&\<close> 55)
+ and lnot (\<open>-- _\<close> [60] 60)
assumes assoc: "(x && y) && z = x && (y && z)"
and notnot: "-- (-- x) = x"
begin
-definition lor (infixl "||" 50) where
+definition lor (infixl \<open>||\<close> 50) where
"x || y = --(-- x && -- y)"
end
@@ -147,8 +147,8 @@
and p2 :: "'b => o"
begin
-definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
-definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \<longleftrightarrow> \<not> p2(x)"
+definition d1 :: "'a => o" (\<open>D1'(_')\<close>) where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
+definition d2 :: "'b => o" (\<open>D2'(_')\<close>) where "d2(x) \<longleftrightarrow> \<not> p2(x)"
thm d1_def d2_def
@@ -191,9 +191,9 @@
section \<open>Defines\<close>
locale logic_def =
- fixes land (infixl "&&" 55)
- and lor (infixl "||" 50)
- and lnot ("-- _" [60] 60)
+ fixes land (infixl \<open>&&\<close> 55)
+ and lor (infixl \<open>||\<close> 50)
+ and lnot (\<open>-- _\<close> [60] 60)
assumes assoc: "(x && y) && z = x && (y && z)"
and notnot: "-- (-- x) = x"
defines "x || y == --(-- x && -- y)"
@@ -353,7 +353,7 @@
(* Duality *)
locale order =
- fixes less :: "'a => 'a => o" (infix "<<" 50)
+ fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
assumes refl: "x << x"
and trans: "[| x << y; y << z |] ==> x << z"
@@ -364,14 +364,14 @@
print_locale! order (* Only two instances of order. *)
locale order' =
- fixes less :: "'a => 'a => o" (infix "<<" 50)
+ fixes less :: "'a => 'a => o" (infix \<open><<\<close> 50)
assumes refl: "x << x"
and trans: "[| x << y; y << z |] ==> x << z"
locale order_with_def = order'
begin
-definition greater :: "'a => 'a => o" (infix ">>" 50) where
+definition greater :: "'a => 'a => o" (infix \<open>>>\<close> 50) where
"x >> y \<longleftrightarrow> y << x"
end
@@ -464,13 +464,13 @@
by unfold_locales (rule int_assoc int_minus2)+
locale logic2 =
- fixes land (infixl "&&" 55)
- and lnot ("-- _" [60] 60)
+ fixes land (infixl \<open>&&\<close> 55)
+ and lnot (\<open>-- _\<close> [60] 60)
assumes assoc: "(x && y) && z = x && (y && z)"
and notnot: "-- (-- x) = x"
begin
-definition lor (infixl "||" 50) where
+definition lor (infixl \<open>||\<close> 50) where
"x || y = --(-- x && -- y)"
end
@@ -495,13 +495,13 @@
subsection \<open>Rewrite morphism\<close>
locale logic_o =
- fixes land (infixl "&&" 55)
- and lnot ("-- _" [60] 60)
+ fixes land (infixl \<open>&&\<close> 55)
+ and lnot (\<open>-- _\<close> [60] 60)
assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
and notnot_o: "-- (-- x) \<longleftrightarrow> x"
begin
-definition lor_o (infixl "||" 50) where
+definition lor_o (infixl \<open>||\<close> 50) where
"x || y \<longleftrightarrow> --(-- x && -- y)"
end
@@ -536,11 +536,11 @@
subsection \<open>Inheritance of rewrite morphisms\<close>
locale reflexive =
- fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
+ fixes le :: "'a => 'a => o" (infix \<open>\<sqsubseteq>\<close> 50)
assumes refl: "x \<sqsubseteq> x"
begin
-definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
+definition less (infix \<open>\<sqsubset>\<close> 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
end
--- a/src/FOL/ex/Nat.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Nat.thy Thu Jan 03 21:15:52 2019 +0100
@@ -13,7 +13,7 @@
instance nat :: "term" ..
axiomatization
- Zero :: nat ("0") and
+ Zero :: nat (\<open>0\<close>) and
Suc :: "nat => nat" and
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
where
@@ -23,7 +23,7 @@
rec_0: "rec(0,a,f) = a" and
rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-definition add :: "[nat, nat] => nat" (infixl "+" 60)
+definition add :: "[nat, nat] => nat" (infixl \<open>+\<close> 60)
where "m + n == rec(m, n, %x y. Suc(y))"
--- a/src/FOL/ex/Natural_Numbers.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Natural_Numbers.thy Thu Jan 03 21:15:52 2019 +0100
@@ -17,7 +17,7 @@
instance nat :: "term" ..
axiomatization
- Zero :: nat ("0") and
+ Zero :: nat (\<open>0\<close>) and
Suc :: "nat => nat" and
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
where
@@ -46,7 +46,7 @@
qed
-definition add :: "nat => nat => nat" (infixl "+" 60)
+definition add :: "nat => nat => nat" (infixl \<open>+\<close> 60)
where "m + n = rec(m, n, \<lambda>x y. Suc(y))"
lemma add_0 [simp]: "0 + n = n"
--- a/src/FOL/ex/Prolog.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/FOL/ex/Prolog.thy Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
axiomatization
Nil :: "'a list" and
- Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and
+ Cons :: "['a, 'a list]=> 'a list" (infixr \<open>:\<close> 60) and
app :: "['a list, 'a list, 'a list] => o" and
rev :: "['a list, 'a list] => o"
where
--- a/src/ZF/Arith.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Arith.thy Thu Jan 03 21:15:52 2019 +0100
@@ -43,15 +43,15 @@
"raw_mult(succ(m), n) = raw_add (n, raw_mult(m, n))"
definition
- add :: "[i,i]=>i" (infixl "#+" 65) where
+ add :: "[i,i]=>i" (infixl \<open>#+\<close> 65) where
"m #+ n == raw_add (natify(m), natify(n))"
definition
- diff :: "[i,i]=>i" (infixl "#-" 65) where
+ diff :: "[i,i]=>i" (infixl \<open>#-\<close> 65) where
"m #- n == raw_diff (natify(m), natify(n))"
definition
- mult :: "[i,i]=>i" (infixl "#*" 70) where
+ mult :: "[i,i]=>i" (infixl \<open>#*\<close> 70) where
"m #* n == raw_mult (natify(m), natify(n))"
definition
@@ -65,11 +65,11 @@
transrec(m, %j f. if j<n | n=0 then j else f`(j#-n))"
definition
- div :: "[i,i]=>i" (infixl "div" 70) where
+ div :: "[i,i]=>i" (infixl \<open>div\<close> 70) where
"m div n == raw_div (natify(m), natify(n))"
definition
- mod :: "[i,i]=>i" (infixl "mod" 70) where
+ mod :: "[i,i]=>i" (infixl \<open>mod\<close> 70) where
"m mod n == raw_mod (natify(m), natify(n))"
declare rec_type [simp]
--- a/src/ZF/Bin.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Bin.thy Thu Jan 03 21:15:52 2019 +0100
@@ -23,7 +23,7 @@
datatype
"bin" = Pls
| Min
- | Bit ("w \<in> bin", "b \<in> bool") (infixl "BIT" 90)
+ | Bit ("w \<in> bin", "b \<in> bool") (infixl \<open>BIT\<close> 90)
consts
integ_of :: "i=>i"
@@ -101,11 +101,11 @@
NCons(bin_mult(v,w),0))"
syntax
- "_Int0" :: i ("#()0")
- "_Int1" :: i ("#()1")
- "_Int2" :: i ("#()2")
- "_Neg_Int1" :: i ("#-()1")
- "_Neg_Int2" :: i ("#-()2")
+ "_Int0" :: i (\<open>#()0\<close>)
+ "_Int1" :: i (\<open>#()1\<close>)
+ "_Int2" :: i (\<open>#()2\<close>)
+ "_Neg_Int1" :: i (\<open>#-()1\<close>)
+ "_Neg_Int2" :: i (\<open>#-()2\<close>)
translations
"#0" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
"#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
@@ -114,8 +114,8 @@
"#-2" \<rightleftharpoons> "CONST integ_of(CONST Min BIT 0)"
syntax
- "_Int" :: "num_token => i" ("#_" 1000)
- "_Neg_Int" :: "num_token => i" ("#-_" 1000)
+ "_Int" :: "num_token => i" (\<open>#_\<close> 1000)
+ "_Neg_Int" :: "num_token => i" (\<open>#-_\<close> 1000)
ML_file "Tools/numeral_syntax.ML"
--- a/src/ZF/Bool.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Bool.thy Thu Jan 03 21:15:52 2019 +0100
@@ -8,11 +8,11 @@
theory Bool imports pair begin
abbreviation
- one ("1") where
+ one (\<open>1\<close>) where
"1 == succ(0)"
abbreviation
- two ("2") where
+ two (\<open>2\<close>) where
"2 == succ(1)"
text\<open>2 is equal to bool, but is used as a number rather than a type.\<close>
@@ -24,15 +24,15 @@
definition "not(b) == cond(b,0,1)"
definition
- "and" :: "[i,i]=>i" (infixl "and" 70) where
+ "and" :: "[i,i]=>i" (infixl \<open>and\<close> 70) where
"a and b == cond(a,b,0)"
definition
- or :: "[i,i]=>i" (infixl "or" 65) where
+ or :: "[i,i]=>i" (infixl \<open>or\<close> 65) where
"a or b == cond(a,1,b)"
definition
- xor :: "[i,i]=>i" (infixl "xor" 65) where
+ xor :: "[i,i]=>i" (infixl \<open>xor\<close> 65) where
"a xor b == cond(a,not(b),b)"
--- a/src/ZF/Cardinal.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Cardinal.thy Thu Jan 03 21:15:52 2019 +0100
@@ -9,23 +9,23 @@
definition
(*least ordinal operator*)
- Least :: "(i=>o) => i" (binder "\<mu> " 10) where
+ Least :: "(i=>o) => i" (binder \<open>\<mu> \<close> 10) where
"Least(P) == THE i. Ord(i) & P(i) & (\<forall>j. j<i \<longrightarrow> ~P(j))"
definition
- eqpoll :: "[i,i] => o" (infixl "\<approx>" 50) where
+ eqpoll :: "[i,i] => o" (infixl \<open>\<approx>\<close> 50) where
"A \<approx> B == \<exists>f. f \<in> bij(A,B)"
definition
- lepoll :: "[i,i] => o" (infixl "\<lesssim>" 50) where
+ lepoll :: "[i,i] => o" (infixl \<open>\<lesssim>\<close> 50) where
"A \<lesssim> B == \<exists>f. f \<in> inj(A,B)"
definition
- lesspoll :: "[i,i] => o" (infixl "\<prec>" 50) where
+ lesspoll :: "[i,i] => o" (infixl \<open>\<prec>\<close> 50) where
"A \<prec> B == A \<lesssim> B & ~(A \<approx> B)"
definition
- cardinal :: "i=>i" ("|_|") where
+ cardinal :: "i=>i" (\<open>|_|\<close>) where
"|A| == (\<mu> i. i \<approx> A)"
definition
--- a/src/ZF/CardinalArith.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/CardinalArith.thy Thu Jan 03 21:15:52 2019 +0100
@@ -12,11 +12,11 @@
"InfCard(i) == Card(i) & nat \<le> i"
definition
- cmult :: "[i,i]=>i" (infixl "\<otimes>" 70) where
+ cmult :: "[i,i]=>i" (infixl \<open>\<otimes>\<close> 70) where
"i \<otimes> j == |i*j|"
definition
- cadd :: "[i,i]=>i" (infixl "\<oplus>" 65) where
+ cadd :: "[i,i]=>i" (infixl \<open>\<oplus>\<close> 65) where
"i \<oplus> j == |i+j|"
definition
--- a/src/ZF/Constructible/L_axioms.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Thu Jan 03 21:15:52 2019 +0100
@@ -130,7 +130,7 @@
text\<open>We must use the meta-existential quantifier; otherwise the reflection
terms become enormous!\<close>
definition
- L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") where
+ L_Reflects :: "[i=>o,[i,i]=>o] => prop" (\<open>(3REFLECTS/ [_,/ _])\<close>) where
"REFLECTS[P,Q] == (\<Or>Cl. Closed_Unbounded(Cl) &
(\<forall>a. Cl(a) \<longrightarrow> (\<forall>x \<in> Lset(a). P(x) \<longleftrightarrow> Q(a,x))))"
@@ -268,25 +268,25 @@
subsubsection\<open>Some numbers to help write de Bruijn indices\<close>
abbreviation
- digit3 :: i ("3") where "3 == succ(2)"
+ digit3 :: i (\<open>3\<close>) where "3 == succ(2)"
abbreviation
- digit4 :: i ("4") where "4 == succ(3)"
+ digit4 :: i (\<open>4\<close>) where "4 == succ(3)"
abbreviation
- digit5 :: i ("5") where "5 == succ(4)"
+ digit5 :: i (\<open>5\<close>) where "5 == succ(4)"
abbreviation
- digit6 :: i ("6") where "6 == succ(5)"
+ digit6 :: i (\<open>6\<close>) where "6 == succ(5)"
abbreviation
- digit7 :: i ("7") where "7 == succ(6)"
+ digit7 :: i (\<open>7\<close>) where "7 == succ(6)"
abbreviation
- digit8 :: i ("8") where "8 == succ(7)"
+ digit8 :: i (\<open>8\<close>) where "8 == succ(7)"
abbreviation
- digit9 :: i ("9") where "9 == succ(8)"
+ digit9 :: i (\<open>9\<close>) where "9 == succ(8)"
subsubsection\<open>The Empty Set, Internalized\<close>
--- a/src/ZF/Constructible/MetaExists.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/MetaExists.thy Thu Jan 03 21:15:52 2019 +0100
@@ -10,7 +10,7 @@
Yields a proposition rather than a FOL formula.\<close>
definition
- ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder "\<Or>" 0) where
+ ex :: "(('a::{}) \<Rightarrow> prop) \<Rightarrow> prop" (binder \<open>\<Or>\<close> 0) where
"ex(P) == (\<And>Q. (\<And>x. PROP P(x) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q)"
lemma meta_exI: "PROP P(x) ==> (\<Or>x. PROP P(x))"
--- a/src/ZF/Constructible/Normal.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Constructible/Normal.thy Thu Jan 03 21:15:52 2019 +0100
@@ -456,7 +456,7 @@
numbers.\<close>
definition
- Aleph :: "i => i" ("\<aleph>_" [90] 90) where
+ Aleph :: "i => i" (\<open>\<aleph>_\<close> [90] 90) where
"Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
lemma Card_Aleph [simp, intro]:
--- a/src/ZF/EquivClass.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/EquivClass.thy Thu Jan 03 21:15:52 2019 +0100
@@ -8,7 +8,7 @@
theory EquivClass imports Trancl Perm begin
definition
- quotient :: "[i,i]=>i" (infixl "'/'/" 90) (*set of equiv classes*) where
+ quotient :: "[i,i]=>i" (infixl \<open>'/'/\<close> 90) (*set of equiv classes*) where
"A//r == {r``{x} . x \<in> A}"
definition
@@ -21,11 +21,11 @@
<y1,z1>:r1 \<longrightarrow> <y2,z2>:r2 \<longrightarrow> b(y1,y2) = b(z1,z2)"
abbreviation
- RESPECTS ::"[i=>i, i] => o" (infixr "respects" 80) where
+ RESPECTS ::"[i=>i, i] => o" (infixr \<open>respects\<close> 80) where
"f respects r == congruent(r,f)"
abbreviation
- RESPECTS2 ::"[i=>i=>i, i] => o" (infixr "respects2 " 80) where
+ RESPECTS2 ::"[i=>i=>i, i] => o" (infixr \<open>respects2 \<close> 80) where
"f respects2 r == congruent2(r,r,f)"
\<comment> \<open>Abbreviation for the common case where the relations are identical\<close>
--- a/src/ZF/Finite.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Finite.thy Thu Jan 03 21:15:52 2019 +0100
@@ -19,7 +19,7 @@
consts
Fin :: "i=>i"
- FiniteFun :: "[i,i]=>i" ("(_ -||>/ _)" [61, 60] 60)
+ FiniteFun :: "[i,i]=>i" (\<open>(_ -||>/ _)\<close> [61, 60] 60)
inductive
domains "Fin(A)" \<subseteq> "Pow(A)"
--- a/src/ZF/IMP/Com.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IMP/Com.thy Thu Jan 03 21:15:52 2019 +0100
@@ -23,7 +23,7 @@
consts evala :: i
abbreviation
- evala_syntax :: "[i, i] => o" (infixl "-a->" 50)
+ evala_syntax :: "[i, i] => o" (infixl \<open>-a->\<close> 50)
where "p -a-> n == <p,n> \<in> evala"
inductive
@@ -46,14 +46,14 @@
| false
| ROp ("f \<in> (nat \<times> nat)->bool", "a0 \<in> aexp", "a1 \<in> aexp")
| noti ("b \<in> bexp")
- | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl "andi" 60)
- | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl "ori" 60)
+ | andi ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>andi\<close> 60)
+ | ori ("b0 \<in> bexp", "b1 \<in> bexp") (infixl \<open>ori\<close> 60)
consts evalb :: i
abbreviation
- evalb_syntax :: "[i,i] => o" (infixl "-b->" 50)
+ evalb_syntax :: "[i,i] => o" (infixl \<open>-b->\<close> 50)
where "p -b-> b == <p,b> \<in> evalb"
inductive
@@ -77,17 +77,17 @@
consts com :: i
datatype com =
- skip ("\<SKIP>" [])
- | assignment ("x \<in> loc", "a \<in> aexp") (infixl "\<ASSN>" 60)
- | semicolon ("c0 \<in> com", "c1 \<in> com") ("_\<SEQ> _" [60, 60] 10)
- | while ("b \<in> bexp", "c \<in> com") ("\<WHILE> _ \<DO> _" 60)
- | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
+ skip (\<open>\<SKIP>\<close> [])
+ | assignment ("x \<in> loc", "a \<in> aexp") (infixl \<open>\<ASSN>\<close> 60)
+ | semicolon ("c0 \<in> com", "c1 \<in> com") (\<open>_\<SEQ> _\<close> [60, 60] 10)
+ | while ("b \<in> bexp", "c \<in> com") (\<open>\<WHILE> _ \<DO> _\<close> 60)
+ | "if" ("b \<in> bexp", "c0 \<in> com", "c1 \<in> com") (\<open>\<IF> _ \<THEN> _ \<ELSE> _\<close> 60)
consts evalc :: i
abbreviation
- evalc_syntax :: "[i, i] => o" (infixl "-c->" 50)
+ evalc_syntax :: "[i, i] => o" (infixl \<open>-c->\<close> 50)
where "p -c-> s == <p,s> \<in> evalc"
inductive
--- a/src/ZF/IMP/Denotation.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IMP/Denotation.thy Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
C :: "i => i"
definition
- Gamma :: "[i,i,i] => i" ("\<Gamma>") where
+ Gamma :: "[i,i,i] => i" (\<open>\<Gamma>\<close>) where
"\<Gamma>(b,cden) ==
(\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>
{io \<in> id(loc->nat). B(b,fst(io))=0})"
--- a/src/ZF/Induct/Comb.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/Comb.thy Thu Jan 03 21:15:52 2019 +0100
@@ -24,7 +24,7 @@
datatype comb =
K
| S
-| app ("p \<in> comb", "q \<in> comb") (infixl "\<bullet>" 90)
+| app ("p \<in> comb", "q \<in> comb") (infixl \<open>\<bullet>\<close> 90)
text \<open>
Inductive definition of contractions, \<open>\<rightarrow>\<^sup>1\<close> and
@@ -32,10 +32,10 @@
\<close>
consts contract :: i
-abbreviation contract_syntax :: "[i,i] \<Rightarrow> o" (infixl "\<rightarrow>\<^sup>1" 50)
+abbreviation contract_syntax :: "[i,i] \<Rightarrow> o" (infixl \<open>\<rightarrow>\<^sup>1\<close> 50)
where "p \<rightarrow>\<^sup>1 q \<equiv> <p,q> \<in> contract"
-abbreviation contract_multi :: "[i,i] \<Rightarrow> o" (infixl "\<rightarrow>" 50)
+abbreviation contract_multi :: "[i,i] \<Rightarrow> o" (infixl \<open>\<rightarrow>\<close> 50)
where "p \<rightarrow> q \<equiv> <p,q> \<in> contract^*"
inductive
@@ -54,10 +54,10 @@
consts parcontract :: i
-abbreviation parcontract_syntax :: "[i,i] => o" (infixl "\<Rrightarrow>\<^sup>1" 50)
+abbreviation parcontract_syntax :: "[i,i] => o" (infixl \<open>\<Rrightarrow>\<^sup>1\<close> 50)
where "p \<Rrightarrow>\<^sup>1 q == <p,q> \<in> parcontract"
-abbreviation parcontract_multi :: "[i,i] => o" (infixl "\<Rrightarrow>" 50)
+abbreviation parcontract_multi :: "[i,i] => o" (infixl \<open>\<Rrightarrow>\<close> 50)
where "p \<Rrightarrow> q == <p,q> \<in> parcontract^+"
inductive
--- a/src/ZF/Induct/FoldSet.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/FoldSet.thy Thu Jan 03 21:15:52 2019 +0100
@@ -19,7 +19,7 @@
type_intros Fin.intros
definition
- fold :: "[i, [i,i]=>i, i, i] => i" ("fold[_]'(_,_,_')") where
+ fold :: "[i, [i,i]=>i, i, i] => i" (\<open>fold[_]'(_,_,_')\<close>) where
"fold[B](f,e, A) == THE x. <A, x>\<in>fold_set(A, B, f,e)"
definition
--- a/src/ZF/Induct/Multiset.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/Multiset.thy Thu Jan 03 21:15:52 2019 +0100
@@ -33,7 +33,7 @@
"mset_of(M) == domain(M)"
definition
- munion :: "[i, i] => i" (infixl "+#" 65) where
+ munion :: "[i, i] => i" (infixl \<open>+#\<close> 65) where
"M +# N == \<lambda>x \<in> mset_of(M) \<union> mset_of(N).
if x \<in> mset_of(M) \<inter> mset_of(N) then (M`x) #+ (N`x)
else (if x \<in> mset_of(M) then M`x else N`x)"
@@ -47,13 +47,13 @@
else 0"
definition
- mdiff :: "[i, i] => i" (infixl "-#" 65) where
+ mdiff :: "[i, i] => i" (infixl \<open>-#\<close> 65) where
"M -# N == normalize(\<lambda>x \<in> mset_of(M).
if x \<in> mset_of(N) then M`x #- N`x else M`x)"
definition
(* set of elements of a multiset *)
- msingle :: "i => i" ("{#_#}") where
+ msingle :: "i => i" (\<open>{#_#}\<close>) where
"{#a#} == {<a, 1>}"
definition
@@ -70,11 +70,11 @@
"msize(M) == setsum(%a. $# mcount(M,a), mset_of(M))"
abbreviation
- melem :: "[i,i] => o" ("(_/ :# _)" [50, 51] 50) where
+ melem :: "[i,i] => o" (\<open>(_/ :# _)\<close> [50, 51] 50) where
"a :# M == a \<in> mset_of(M)"
syntax
- "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+ "_MColl" :: "[pttrn, i, o] => i" (\<open>(1{# _ \<in> _./ _#})\<close>)
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
@@ -100,11 +100,11 @@
"omultiset(M) == \<exists>i. Ord(i) & M \<in> Mult(field(Memrel(i)))"
definition
- mless :: "[i, i] => o" (infixl "<#" 50) where
+ mless :: "[i, i] => o" (infixl \<open><#\<close> 50) where
"M <# N == \<exists>i. Ord(i) & <M, N> \<in> multirel(field(Memrel(i)), Memrel(i))"
definition
- mle :: "[i, i] => o" (infixl "<#=" 50) where
+ mle :: "[i, i] => o" (infixl \<open><#=\<close> 50) where
"M <#= N == (omultiset(M) & M = N) | M <# N"
--- a/src/ZF/Induct/PropLog.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Induct/PropLog.thy Thu Jan 03 21:15:52 2019 +0100
@@ -26,8 +26,8 @@
datatype propn =
Fls
- | Var ("n \<in> nat") ("#_" [100] 100)
- | Imp ("p \<in> propn", "q \<in> propn") (infixr "=>" 90)
+ | Var ("n \<in> nat") (\<open>#_\<close> [100] 100)
+ | Imp ("p \<in> propn", "q \<in> propn") (infixr \<open>=>\<close> 90)
subsection \<open>The proof system\<close>
@@ -35,7 +35,7 @@
consts thms :: "i => i"
abbreviation
- thms_syntax :: "[i,i] => o" (infixl "|-" 50)
+ thms_syntax :: "[i,i] => o" (infixl \<open>|-\<close> 50)
where "H |- p == p \<in> thms(H)"
inductive
@@ -86,7 +86,7 @@
\<close>
definition
- logcon :: "[i,i] => o" (infixl "|=" 50) where
+ logcon :: "[i,i] => o" (infixl \<open>|=\<close> 50) where
"H |= p == \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
--- a/src/ZF/Int.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Int.thy Thu Jan 03 21:15:52 2019 +0100
@@ -17,7 +17,7 @@
"int == (nat*nat)//intrel"
definition
- int_of :: "i=>i" \<comment> \<open>coercion from nat to int\<close> ("$# _" [80] 80) where
+ int_of :: "i=>i" \<comment> \<open>coercion from nat to int\<close> (\<open>$# _\<close> [80] 80) where
"$# m == intrel `` {<natify(m), 0>}"
definition
@@ -29,7 +29,7 @@
"raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"
definition
- zminus :: "i=>i" ("$- _" [80] 80) where
+ zminus :: "i=>i" (\<open>$- _\<close> [80] 80) where
"$- z == raw_zminus (intify(z))"
definition
@@ -65,7 +65,7 @@
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
definition
- zmult :: "[i,i]=>i" (infixl "$*" 70) where
+ zmult :: "[i,i]=>i" (infixl \<open>$*\<close> 70) where
"z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
definition
@@ -75,19 +75,19 @@
in intrel``{<x1#+x2, y1#+y2>}"
definition
- zadd :: "[i,i]=>i" (infixl "$+" 65) where
+ zadd :: "[i,i]=>i" (infixl \<open>$+\<close> 65) where
"z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
definition
- zdiff :: "[i,i]=>i" (infixl "$-" 65) where
+ zdiff :: "[i,i]=>i" (infixl \<open>$-\<close> 65) where
"z1 $- z2 == z1 $+ zminus(z2)"
definition
- zless :: "[i,i]=>o" (infixl "$<" 50) where
+ zless :: "[i,i]=>o" (infixl \<open>$<\<close> 50) where
"z1 $< z2 == znegative(z1 $- z2)"
definition
- zle :: "[i,i]=>o" (infixl "$\<le>" 50) where
+ zle :: "[i,i]=>o" (infixl \<open>$\<le>\<close> 50) where
"z1 $\<le> z2 == z1 $< z2 | intify(z1)=intify(z2)"
--- a/src/ZF/IntDiv.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/IntDiv.thy Thu Jan 03 21:15:52 2019 +0100
@@ -88,11 +88,11 @@
else negateSnd (posDivAlg (<$-a,$-b>))"
definition
- zdiv :: "[i,i]=>i" (infixl "zdiv" 70) where
+ zdiv :: "[i,i]=>i" (infixl \<open>zdiv\<close> 70) where
"a zdiv b == fst (divAlg (<intify(a), intify(b)>))"
definition
- zmod :: "[i,i]=>i" (infixl "zmod" 70) where
+ zmod :: "[i,i]=>i" (infixl \<open>zmod\<close> 70) where
"a zmod b == snd (divAlg (<intify(a), intify(b)>))"
--- a/src/ZF/List.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/List.thy Thu Jan 03 21:15:52 2019 +0100
@@ -15,8 +15,8 @@
syntax
- "_Nil" :: i ("[]")
- "_List" :: "is => i" ("[(_)]")
+ "_Nil" :: i (\<open>[]\<close>)
+ "_List" :: "is => i" (\<open>[(_)]\<close>)
translations
"[x, xs]" == "CONST Cons(x, [xs])"
@@ -45,7 +45,7 @@
consts
map :: "[i=>i, i] => i"
set_of_list :: "i=>i"
- app :: "[i,i]=>i" (infixr "@" 60)
+ app :: "[i,i]=>i" (infixr \<open>@\<close> 60)
(*map is a binding operator -- it applies to meta-level functions, not
object-level functions. This simplifies the final form of term_rec_conv,
--- a/src/ZF/OrdQuant.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/OrdQuant.thy Thu Jan 03 21:15:52 2019 +0100
@@ -23,9 +23,9 @@
"OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
syntax
- "_oall" :: "[idt, i, o] => o" ("(3\<forall>_<_./ _)" 10)
- "_oex" :: "[idt, i, o] => o" ("(3\<exists>_<_./ _)" 10)
- "_OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+ "_oall" :: "[idt, i, o] => o" (\<open>(3\<forall>_<_./ _)\<close> 10)
+ "_oex" :: "[idt, i, o] => o" (\<open>(3\<exists>_<_./ _)\<close> 10)
+ "_OUNION" :: "[idt, i, i] => i" (\<open>(3\<Union>_<_./ _)\<close> 10)
translations
"\<forall>x<a. P" \<rightleftharpoons> "CONST oall(a, \<lambda>x. P)"
"\<exists>x<a. P" \<rightleftharpoons> "CONST oex(a, \<lambda>x. P)"
@@ -192,8 +192,8 @@
"rex(M, P) == \<exists>x. M(x) & P(x)"
syntax
- "_rall" :: "[pttrn, i=>o, o] => o" ("(3\<forall>_[_]./ _)" 10)
- "_rex" :: "[pttrn, i=>o, o] => o" ("(3\<exists>_[_]./ _)" 10)
+ "_rall" :: "[pttrn, i=>o, o] => o" (\<open>(3\<forall>_[_]./ _)\<close> 10)
+ "_rex" :: "[pttrn, i=>o, o] => o" (\<open>(3\<exists>_[_]./ _)\<close> 10)
translations
"\<forall>x[M]. P" \<rightleftharpoons> "CONST rall(M, \<lambda>x. P)"
"\<exists>x[M]. P" \<rightleftharpoons> "CONST rex(M, \<lambda>x. P)"
@@ -323,7 +323,7 @@
subsubsection\<open>Sets as Classes\<close>
definition
- setclass :: "[i,i] => o" ("##_" [40] 40) where
+ setclass :: "[i,i] => o" (\<open>##_\<close> [40] 40) where
"setclass(A) == %x. x \<in> A"
lemma setclass_iff [simp]: "setclass(A,x) <-> x \<in> A"
--- a/src/ZF/Order.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Order.thy Thu Jan 03 21:15:52 2019 +0100
@@ -49,7 +49,7 @@
{f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longrightarrow> <f`x,f`y>:s}"
definition
- ord_iso :: "[i,i,i,i]=>i" ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51) (*Order isomorphisms*) where
+ ord_iso :: "[i,i,i,i]=>i" (\<open>(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51) (*Order isomorphisms*) where
"\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> ==
{f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. <x,y>:r \<longleftrightarrow> <f`x,f`y>:s}"
--- a/src/ZF/OrderType.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/OrderType.thy Thu Jan 03 21:15:52 2019 +0100
@@ -31,7 +31,7 @@
definition
(*ordinal multiplication*)
- omult :: "[i,i]=>i" (infixl "**" 70) where
+ omult :: "[i,i]=>i" (infixl \<open>**\<close> 70) where
"i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
definition
@@ -40,12 +40,12 @@
"raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
definition
- oadd :: "[i,i]=>i" (infixl "++" 65) where
+ oadd :: "[i,i]=>i" (infixl \<open>++\<close> 65) where
"i ++ j == raw_oadd(ordify(i),ordify(j))"
definition
(*ordinal subtraction*)
- odiff :: "[i,i]=>i" (infixl "--" 65) where
+ odiff :: "[i,i]=>i" (infixl \<open>--\<close> 65) where
"i -- j == ordertype(i-j, Memrel(i))"
--- a/src/ZF/Ordinal.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Ordinal.thy Thu Jan 03 21:15:52 2019 +0100
@@ -20,7 +20,7 @@
"Ord(i) == Transset(i) & (\<forall>x\<in>i. Transset(x))"
definition
- lt :: "[i,i] => o" (infixl "<" 50) (*less-than on ordinals*) where
+ lt :: "[i,i] => o" (infixl \<open><\<close> 50) (*less-than on ordinals*) where
"i<j == i\<in>j & Ord(j)"
definition
@@ -28,7 +28,7 @@
"Limit(i) == Ord(i) & 0<i & (\<forall>y. y<i \<longrightarrow> succ(y)<i)"
abbreviation
- le (infixl "\<le>" 50) where
+ le (infixl \<open>\<le>\<close> 50) where
"x \<le> y == x < succ(y)"
--- a/src/ZF/Perm.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Perm.thy Thu Jan 03 21:15:52 2019 +0100
@@ -14,7 +14,7 @@
definition
(*composition of relations and functions; NOT Suppes's relative product*)
- comp :: "[i,i]=>i" (infixr "O" 60) where
+ comp :: "[i,i]=>i" (infixr \<open>O\<close> 60) where
"r O s == {xz \<in> domain(s)*range(r) .
\<exists>x y z. xz=<x,z> & <x,y>:s & <y,z>:r}"
--- a/src/ZF/QPair.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/QPair.thy Thu Jan 03 21:15:52 2019 +0100
@@ -21,7 +21,7 @@
\<close>
definition
- QPair :: "[i, i] => i" ("<(_;/ _)>") where
+ QPair :: "[i, i] => i" (\<open><(_;/ _)>\<close>) where
"<a;b> == a+b"
definition
@@ -45,16 +45,16 @@
"QSigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
- "_QSUM" :: "[idt, i, i] => i" ("(3QSUM _ \<in> _./ _)" 10)
+ "_QSUM" :: "[idt, i, i] => i" (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
translations
"QSUM x \<in> A. B" => "CONST QSigma(A, %x. B)"
abbreviation
- qprod (infixr "<*>" 80) where
+ qprod (infixr \<open><*>\<close> 80) where
"A <*> B == QSigma(A, %_. B)"
definition
- qsum :: "[i,i]=>i" (infixr "<+>" 65) where
+ qsum :: "[i,i]=>i" (infixr \<open><+>\<close> 65) where
"A <+> B == ({0} <*> A) \<union> ({1} <*> B)"
definition
--- a/src/ZF/Resid/Confluence.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Confluence.thy Thu Jan 03 21:15:52 2019 +0100
@@ -68,11 +68,11 @@
Sconv :: "i"
abbreviation
- Sconv1_rel (infixl "<-1->" 50) where
+ Sconv1_rel (infixl \<open><-1->\<close> 50) where
"a<-1->b == <a,b> \<in> Sconv1"
abbreviation
- Sconv_rel (infixl "<-\<longrightarrow>" 50) where
+ Sconv_rel (infixl \<open><-\<longrightarrow>\<close> 50) where
"a<-\<longrightarrow>b == <a,b> \<in> Sconv"
inductive
--- a/src/ZF/Resid/Redex.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Redex.thy Thu Jan 03 21:15:52 2019 +0100
@@ -18,11 +18,11 @@
Sreg :: "i"
abbreviation
- Ssub_rel (infixl "\<Longleftarrow>" 70) where
+ Ssub_rel (infixl \<open>\<Longleftarrow>\<close> 70) where
"a \<Longleftarrow> b == <a,b> \<in> Ssub"
abbreviation
- Scomp_rel (infixl "\<sim>" 70) where
+ Scomp_rel (infixl \<open>\<sim>\<close> 70) where
"a \<sim> b == <a,b> \<in> Scomp"
abbreviation
@@ -43,7 +43,7 @@
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
definition
- union (infixl "\<squnion>" 70) where
+ union (infixl \<open>\<squnion>\<close> 70) where
"u \<squnion> v == union_aux(u)`v"
--- a/src/ZF/Resid/Reduction.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Reduction.thy Thu Jan 03 21:15:52 2019 +0100
@@ -74,19 +74,19 @@
Spar_red :: "i"
abbreviation
- Sred1_rel (infixl "-1->" 50) where
+ Sred1_rel (infixl \<open>-1->\<close> 50) where
"a -1-> b == <a,b> \<in> Sred1"
abbreviation
- Sred_rel (infixl "-\<longrightarrow>" 50) where
+ Sred_rel (infixl \<open>-\<longrightarrow>\<close> 50) where
"a -\<longrightarrow> b == <a,b> \<in> Sred"
abbreviation
- Spar_red1_rel (infixl "=1=>" 50) where
+ Spar_red1_rel (infixl \<open>=1=>\<close> 50) where
"a =1=> b == <a,b> \<in> Spar_red1"
abbreviation
- Spar_red_rel (infixl "===>" 50) where
+ Spar_red_rel (infixl \<open>===>\<close> 50) where
"a ===> b == <a,b> \<in> Spar_red"
--- a/src/ZF/Resid/Residuals.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Residuals.thy Thu Jan 03 21:15:52 2019 +0100
@@ -26,7 +26,7 @@
type_intros subst_type nat_typechecks redexes.intros bool_typechecks
definition
- res_func :: "[i,i]=>i" (infixl "|>" 70) where
+ res_func :: "[i,i]=>i" (infixl \<open>|>\<close> 70) where
"u |> v == THE w. residuals(u,v,w)"
--- a/src/ZF/Resid/Substitution.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Resid/Substitution.thy Thu Jan 03 21:15:52 2019 +0100
@@ -42,7 +42,7 @@
"subst_rec(u,r,k) == subst_aux(r)`u`k"
abbreviation
- subst :: "[i,i]=>i" (infixl "'/" 70) where
+ subst :: "[i,i]=>i" (infixl \<open>'/\<close> 70) where
"u/v == subst_rec(u,v,0)"
--- a/src/ZF/Sum.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Sum.thy Thu Jan 03 21:15:52 2019 +0100
@@ -9,7 +9,7 @@
text\<open>And the "Part" primitive for simultaneous recursive type definitions\<close>
-definition sum :: "[i,i]=>i" (infixr "+" 65) where
+definition sum :: "[i,i]=>i" (infixr \<open>+\<close> 65) where
"A+B == {0}*A \<union> {1}*B"
definition Inl :: "i=>i" where
--- a/src/ZF/Trancl.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/Trancl.thy Thu Jan 03 21:15:52 2019 +0100
@@ -32,16 +32,16 @@
"trans(r) == \<forall>x y z. <x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
definition
- trans_on :: "[i,i]=>o" ("trans[_]'(_')") where
+ trans_on :: "[i,i]=>o" (\<open>trans[_]'(_')\<close>) where
"trans[A](r) == \<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A.
<x,y>: r \<longrightarrow> <y,z>: r \<longrightarrow> <x,z>: r"
definition
- rtrancl :: "i=>i" ("(_^*)" [100] 100) (*refl/transitive closure*) where
+ rtrancl :: "i=>i" (\<open>(_^*)\<close> [100] 100) (*refl/transitive closure*) where
"r^* == lfp(field(r)*field(r), %s. id(field(r)) \<union> (r O s))"
definition
- trancl :: "i=>i" ("(_^+)" [100] 100) (*transitive closure*) where
+ trancl :: "i=>i" (\<open>(_^+)\<close> [100] 100) (*transitive closure*) where
"r^+ == r O r^*"
definition
--- a/src/ZF/UNITY/Comp.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Comp.thy Thu Jan 03 21:15:52 2019 +0100
@@ -18,20 +18,20 @@
theory Comp imports Union Increasing begin
definition
- component :: "[i,i]=>o" (infixl "component" 65) where
+ component :: "[i,i]=>o" (infixl \<open>component\<close> 65) where
"F component H == (\<exists>G. F \<squnion> G = H)"
definition
- strict_component :: "[i,i]=>o" (infixl "strict'_component" 65) where
+ strict_component :: "[i,i]=>o" (infixl \<open>strict'_component\<close> 65) where
"F strict_component H == F component H & F\<noteq>H"
definition
(* A stronger form of the component relation *)
- component_of :: "[i,i]=>o" (infixl "component'_of" 65) where
+ component_of :: "[i,i]=>o" (infixl \<open>component'_of\<close> 65) where
"F component_of H == (\<exists>G. F ok G & F \<squnion> G = H)"
definition
- strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) where
+ strict_component_of :: "[i,i]=>o" (infixl \<open>strict'_component'_of\<close> 65) where
"F strict_component_of H == F component_of H & F\<noteq>H"
definition
--- a/src/ZF/UNITY/Constrains.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Constrains.thy Thu Jan 03 21:15:52 2019 +0100
@@ -40,11 +40,11 @@
definition
- Constrains :: "[i,i] => i" (infixl "Co" 60) where
+ Constrains :: "[i,i] => i" (infixl \<open>Co\<close> 60) where
"A Co B == {F:program. F:(reachable(F) \<inter> A) co B}"
definition
- op_Unless :: "[i, i] => i" (infixl "Unless" 60) where
+ op_Unless :: "[i, i] => i" (infixl \<open>Unless\<close> 60) where
"A Unless B == (A-B) Co (A \<union> B)"
definition
--- a/src/ZF/UNITY/Follows.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Follows.thy Thu Jan 03 21:15:52 2019 +0100
@@ -34,12 +34,12 @@
"m_Incr(f) == Increasing(Mult(nat), MultLe(nat, Le), f)"
abbreviation
- n_Fols :: "[i=>i, i=>i]=>i" (infixl "n'_Fols" 65) where
+ n_Fols :: "[i=>i, i=>i]=>i" (infixl \<open>n'_Fols\<close> 65) where
"f n_Fols g == Follows(nat, Le, f, g)"
abbreviation
Follows' :: "[i=>i, i=>i, i, i] => i"
- ("(_ /Fols _ /Wrt (_ /'/ _))" [60, 0, 0, 60] 60) where
+ (\<open>(_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60) where
"f Fols g Wrt r/A == Follows(A,r,f,g)"
--- a/src/ZF/UNITY/GenPrefix.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Thu Jan 03 21:15:52 2019 +0100
@@ -49,11 +49,11 @@
(* less or equal and greater or equal over prefixes *)
abbreviation
- pfixLe :: "[i, i] => o" (infixl "pfixLe" 50) where
+ pfixLe :: "[i, i] => o" (infixl \<open>pfixLe\<close> 50) where
"xs pfixLe ys == <xs, ys>:gen_prefix(nat, Le)"
abbreviation
- pfixGe :: "[i, i] => o" (infixl "pfixGe" 50) where
+ pfixGe :: "[i, i] => o" (infixl \<open>pfixGe\<close> 50) where
"xs pfixGe ys == <xs, ys>:gen_prefix(nat, Ge)"
--- a/src/ZF/UNITY/Guar.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Guar.thy Thu Jan 03 21:15:52 2019 +0100
@@ -57,7 +57,7 @@
(SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))"
definition
- guar :: "[i, i] => i" (infixl "guarantees" 55) where
+ guar :: "[i, i] => i" (infixl \<open>guarantees\<close> 55) where
(*higher than membership, lower than Co*)
"X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X \<longrightarrow> F \<squnion> G \<in> Y}"
@@ -77,13 +77,13 @@
"welldef == {F \<in> program. Init(F) \<noteq> 0}"
definition
- refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10) where
+ refines :: "[i, i, i] => o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10) where
"G refines F wrt X ==
\<forall>H \<in> program. (F ok H & G ok H & F \<squnion> H \<in> welldef \<inter> X)
\<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
definition
- iso_refines :: "[i,i, i] => o" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where
+ iso_refines :: "[i,i, i] => o" (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10) where
"G iso_refines F wrt X == F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
--- a/src/ZF/UNITY/Increasing.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Increasing.thy Thu Jan 03 21:15:52 2019 +0100
@@ -11,19 +11,19 @@
theory Increasing imports Constrains Monotonicity begin
definition
- increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") where
+ increasing :: "[i, i, i=>i] => i" (\<open>increasing[_]'(_, _')\<close>) where
"increasing[A](r, f) ==
{F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) &
(\<forall>x \<in> state. f(x):A)}"
definition
- Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')") where
+ Increasing :: "[i, i, i=>i] => i" (\<open>Increasing[_]'(_, _')\<close>) where
"Increasing[A](r, f) ==
{F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) &
(\<forall>x \<in> state. f(x):A)}"
abbreviation (input)
- IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) where
+ IncWrt :: "[i=>i, i, i] => i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60) where
"f IncreasingWrt r/A == Increasing[A](r,f)"
--- a/src/ZF/UNITY/SubstAx.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Thu Jan 03 21:15:52 2019 +0100
@@ -13,11 +13,11 @@
definition
(* The definitions below are not `conventional', but yield simpler rules *)
- Ensures :: "[i,i] => i" (infixl "Ensures" 60) where
+ Ensures :: "[i,i] => i" (infixl \<open>Ensures\<close> 60) where
"A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }"
definition
- LeadsTo :: "[i, i] => i" (infixl "\<longmapsto>w" 60) where
+ LeadsTo :: "[i, i] => i" (infixl \<open>\<longmapsto>w\<close> 60) where
"A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}"
--- a/src/ZF/UNITY/UNITY.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/UNITY.thy Thu Jan 03 21:15:52 2019 +0100
@@ -27,7 +27,7 @@
cons(id(state), allowed \<inter> Pow(state*state))>"
definition
- SKIP :: i ("\<bottom>") where
+ SKIP :: i (\<open>\<bottom>\<close>) where
"SKIP == mk_program(state, 0, Pow(state*state))"
(* Coercion from anything to program *)
@@ -68,12 +68,12 @@
initially :: "i=>i" where
"initially(A) == {F \<in> program. Init(F)\<subseteq>A}"
-definition "constrains" :: "[i, i] => i" (infixl "co" 60) where
+definition "constrains" :: "[i, i] => i" (infixl \<open>co\<close> 60) where
"A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}"
\<comment> \<open>the condition @{term "st_set(A)"} makes the definition slightly
stronger than the HOL one\<close>
-definition unless :: "[i, i] => i" (infixl "unless" 60) where
+definition unless :: "[i, i] => i" (infixl \<open>unless\<close> 60) where
"A unless B == (A - B) co (A \<union> B)"
definition
@@ -90,7 +90,7 @@
(* meta-function composition *)
definition
- metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65) where
+ metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl \<open>comp\<close> 65) where
"f comp g == %x. f(g(x))"
definition
--- a/src/ZF/UNITY/Union.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/Union.thy Thu Jan 03 21:15:52 2019 +0100
@@ -15,7 +15,7 @@
definition
(*FIXME: conjoin Init(F) \<inter> Init(G) \<noteq> 0 *)
- ok :: "[i, i] => o" (infixl "ok" 65) where
+ ok :: "[i, i] => o" (infixl \<open>ok\<close> 65) where
"F ok G == Acts(F) \<subseteq> AllowedActs(G) &
Acts(G) \<subseteq> AllowedActs(F)"
@@ -31,7 +31,7 @@
\<Inter>i \<in> I. AllowedActs(F(i)))"
definition
- Join :: "[i, i] => i" (infixl "\<squnion>" 65) where
+ Join :: "[i, i] => i" (infixl \<open>\<squnion>\<close> 65) where
"F \<squnion> G == mk_program (Init(F) \<inter> Init(G), Acts(F) \<union> Acts(G),
AllowedActs(F) \<inter> AllowedActs(G))"
definition
@@ -41,8 +41,8 @@
SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
syntax
- "_JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion>_./ _)" 10)
- "_JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion>_ \<in> _./ _)" 10)
+ "_JOIN1" :: "[pttrns, i] => i" (\<open>(3\<Squnion>_./ _)\<close> 10)
+ "_JOIN" :: "[pttrn, i, i] => i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
translations
"\<Squnion>x \<in> A. B" == "CONST JOIN(A, (\<lambda>x. B))"
--- a/src/ZF/UNITY/WFair.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/UNITY/WFair.thy Thu Jan 03 21:15:52 2019 +0100
@@ -21,7 +21,7 @@
act``A \<subseteq> state-A) & st_set(A)}"
definition
- ensures :: "[i,i] => i" (infixl "ensures" 60) where
+ ensures :: "[i,i] => i" (infixl \<open>ensures\<close> 60) where
"A ensures B == ((A-B) co (A \<union> B)) \<inter> transient(A-B)"
consts
@@ -43,7 +43,7 @@
definition
(* The Visible version of the LEADS-TO relation*)
- leadsTo :: "[i, i] => i" (infixl "\<longmapsto>" 60) where
+ leadsTo :: "[i, i] => i" (infixl \<open>\<longmapsto>\<close> 60) where
"A \<longmapsto> B == {F \<in> program. <A,B>:leads(state, F)}"
definition
--- a/src/ZF/WF.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/WF.thy Thu Jan 03 21:15:52 2019 +0100
@@ -24,7 +24,7 @@
"wf(r) == \<forall>Z. Z=0 | (\<exists>x\<in>Z. \<forall>y. <y,x>:r \<longrightarrow> ~ y \<in> Z)"
definition
- wf_on :: "[i,i]=>o" ("wf[_]'(_')") where
+ wf_on :: "[i,i]=>o" (\<open>wf[_]'(_')\<close>) where
(*r is well-founded on A*)
"wf_on(A,r) == wf(r \<inter> A*A)"
@@ -46,7 +46,7 @@
"wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
definition
- wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')") where
+ wfrec_on :: "[i, i, i, [i,i]=>i] =>i" (\<open>wfrec[_]'(_,_,_')\<close>) where
"wfrec[A](r,a,H) == wfrec(r \<inter> A*A, a, H)"
--- a/src/ZF/ZF.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ZF.thy Thu Jan 03 21:15:52 2019 +0100
@@ -7,14 +7,14 @@
subsection\<open>Iteration of the function @{term F}\<close>
-consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60)
+consts iterates :: "[i=>i,i,i] => i" (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
primrec
"F^0 (x) = x"
"F^(succ(n)) (x) = F(F^n (x))"
definition
- iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
+ iterates_omega :: "[i=>i,i] => i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
"F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
lemma iterates_triv:
--- a/src/ZF/ZF_Base.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ZF_Base.thy Thu Jan 03 21:15:52 2019 +0100
@@ -16,14 +16,14 @@
typedecl i
instance i :: "term" ..
-axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl "\<in>" 50) \<comment> \<open>membership relation\<close>
- and zero :: "i" ("0") \<comment> \<open>the empty set\<close>
+axiomatization mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<in>\<close> 50) \<comment> \<open>membership relation\<close>
+ and zero :: "i" (\<open>0\<close>) \<comment> \<open>the empty set\<close>
and Pow :: "i \<Rightarrow> i" \<comment> \<open>power sets\<close>
and Inf :: "i" \<comment> \<open>infinite set\<close>
- and Union :: "i \<Rightarrow> i" ("\<Union>_" [90] 90)
+ and Union :: "i \<Rightarrow> i" (\<open>\<Union>_\<close> [90] 90)
and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
-abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl "\<notin>" 50) \<comment> \<open>negated membership relation\<close>
+abbreviation not_mem :: "[i, i] \<Rightarrow> o" (infixl \<open>\<notin>\<close> 50) \<comment> \<open>negated membership relation\<close>
where "x \<notin> y \<equiv> \<not> (x \<in> y)"
@@ -36,8 +36,8 @@
where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
syntax
- "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<forall>_\<in>_./ _)" 10)
- "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" ("(3\<exists>_\<in>_./ _)" 10)
+ "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
+ "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
translations
"\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
"\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
@@ -52,7 +52,7 @@
where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
syntax
- "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
translations
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
@@ -63,7 +63,7 @@
where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
syntax
- "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \<in> _})" [51,0,51])
+ "_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
translations
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
@@ -74,19 +74,19 @@
where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
syntax
- "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" ("(1{_ \<in> _ ./ _})")
+ "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>)
translations
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
subsection \<open>General union and intersection\<close>
-definition Inter :: "i => i" ("\<Inter>_" [90] 90)
+definition Inter :: "i => i" (\<open>\<Inter>_\<close> [90] 90)
where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
syntax
- "_UNION" :: "[pttrn, i, i] => i" ("(3\<Union>_\<in>_./ _)" 10)
- "_INTER" :: "[pttrn, i, i] => i" ("(3\<Inter>_\<in>_./ _)" 10)
+ "_UNION" :: "[pttrn, i, i] => i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
+ "_INTER" :: "[pttrn, i, i] => i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
translations
"\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
"\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
@@ -100,16 +100,16 @@
definition Upair :: "[i, i] => i"
where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
-definition Subset :: "[i, i] \<Rightarrow> o" (infixl "\<subseteq>" 50) \<comment> \<open>subset relation\<close>
+definition Subset :: "[i, i] \<Rightarrow> o" (infixl \<open>\<subseteq>\<close> 50) \<comment> \<open>subset relation\<close>
where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
-definition Diff :: "[i, i] \<Rightarrow> i" (infixl "-" 65) \<comment> \<open>set difference\<close>
+definition Diff :: "[i, i] \<Rightarrow> i" (infixl \<open>-\<close> 65) \<comment> \<open>set difference\<close>
where "A - B == { x\<in>A . ~(x\<in>B) }"
-definition Un :: "[i, i] \<Rightarrow> i" (infixl "\<union>" 65) \<comment> \<open>binary union\<close>
+definition Un :: "[i, i] \<Rightarrow> i" (infixl \<open>\<union>\<close> 65) \<comment> \<open>binary union\<close>
where "A \<union> B == \<Union>(Upair(A,B))"
-definition Int :: "[i, i] \<Rightarrow> i" (infixl "\<inter>" 70) \<comment> \<open>binary intersection\<close>
+definition Int :: "[i, i] \<Rightarrow> i" (infixl \<open>\<inter>\<close> 70) \<comment> \<open>binary intersection\<close>
where "A \<inter> B == \<Inter>(Upair(A,B))"
definition cons :: "[i, i] => i"
@@ -120,9 +120,9 @@
nonterminal "is"
syntax
- "" :: "i \<Rightarrow> is" ("_")
- "_Enum" :: "[i, is] \<Rightarrow> is" ("_,/ _")
- "_Finset" :: "is \<Rightarrow> i" ("{(_)}")
+ "" :: "i \<Rightarrow> is" (\<open>_\<close>)
+ "_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>)
+ "_Finset" :: "is \<Rightarrow> i" (\<open>{(_)}\<close>)
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
@@ -153,14 +153,14 @@
subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
-definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder "THE " 10)
+definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder \<open>THE \<close> 10)
where the_def: "The(P) == \<Union>({y . x \<in> {0}, P(y)})"
-definition If :: "[o, i, i] \<Rightarrow> i" ("(if (_)/ then (_)/ else (_))" [10] 10)
+definition If :: "[o, i, i] \<Rightarrow> i" (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10)
where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
abbreviation (input)
- old_if :: "[o, i, i] => i" ("if '(_,_,_')")
+ old_if :: "[o, i, i] => i" (\<open>if '(_,_,_')\<close>)
where "if(P,a,b) == If(P,a,b)"
@@ -182,10 +182,10 @@
(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
nonterminal patterns
syntax
- "_pattern" :: "patterns => pttrn" ("\<langle>_\<rangle>")
- "" :: "pttrn => patterns" ("_")
- "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_")
- "_Tuple" :: "[i, is] => i" ("\<langle>(_,/ _)\<rangle>")
+ "_pattern" :: "patterns => pttrn" (\<open>\<langle>_\<rangle>\<close>)
+ "" :: "pttrn => patterns" (\<open>_\<close>)
+ "_patterns" :: "[pttrn, patterns] => patterns" (\<open>_,/_\<close>)
+ "_Tuple" :: "[i, is] => i" (\<open>\<langle>(_,/ _)\<rangle>\<close>)
translations
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
@@ -195,7 +195,7 @@
definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
-abbreviation cart_prod :: "[i, i] => i" (infixr "\<times>" 80) \<comment> \<open>Cartesian product\<close>
+abbreviation cart_prod :: "[i, i] => i" (infixr \<open>\<times>\<close> 80) \<comment> \<open>Cartesian product\<close>
where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
@@ -220,10 +220,10 @@
definition "function" :: "i \<Rightarrow> o" \<comment> \<open>recognizes functions; can have non-pairs\<close>
where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
-definition Image :: "[i, i] \<Rightarrow> i" (infixl "``" 90) \<comment> \<open>image\<close>
+definition Image :: "[i, i] \<Rightarrow> i" (infixl \<open>``\<close> 90) \<comment> \<open>image\<close>
where image_def: "r `` A == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
-definition vimage :: "[i, i] \<Rightarrow> i" (infixl "-``" 90) \<comment> \<open>inverse image\<close>
+definition vimage :: "[i, i] \<Rightarrow> i" (infixl \<open>-``\<close> 90) \<comment> \<open>inverse image\<close>
where vimage_def: "r -`` A == converse(r)``A"
(* Restrict the relation r to the domain A *)
@@ -236,22 +236,22 @@
definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
-definition "apply" :: "[i, i] \<Rightarrow> i" (infixl "`" 90) \<comment> \<open>function application\<close>
+definition "apply" :: "[i, i] \<Rightarrow> i" (infixl \<open>`\<close> 90) \<comment> \<open>function application\<close>
where "f`a == \<Union>(f``{a})"
definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
-abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr "->" 60) \<comment> \<open>function space\<close>
+abbreviation function_space :: "[i, i] \<Rightarrow> i" (infixr \<open>->\<close> 60) \<comment> \<open>function space\<close>
where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
(* binder syntax *)
syntax
- "_PROD" :: "[pttrn, i, i] => i" ("(3\<Prod>_\<in>_./ _)" 10)
- "_SUM" :: "[pttrn, i, i] => i" ("(3\<Sum>_\<in>_./ _)" 10)
- "_lam" :: "[pttrn, i, i] => i" ("(3\<lambda>_\<in>_./ _)" 10)
+ "_PROD" :: "[pttrn, i, i] => i" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
+ "_SUM" :: "[pttrn, i, i] => i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
+ "_lam" :: "[pttrn, i, i] => i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
translations
"\<Prod>x\<in>A. B" == "CONST Pi(A, \<lambda>x. B)"
"\<Sum>x\<in>A. B" == "CONST Sigma(A, \<lambda>x. B)"
@@ -261,27 +261,27 @@
subsection \<open>ASCII syntax\<close>
notation (ASCII)
- cart_prod (infixr "*" 80) and
- Int (infixl "Int" 70) and
- Un (infixl "Un" 65) and
- function_space (infixr "\<rightarrow>" 60) and
- Subset (infixl "<=" 50) and
- mem (infixl ":" 50) and
- not_mem (infixl "~:" 50)
+ cart_prod (infixr \<open>*\<close> 80) and
+ Int (infixl \<open>Int\<close> 70) and
+ Un (infixl \<open>Un\<close> 65) and
+ function_space (infixr \<open>\<rightarrow>\<close> 60) and
+ Subset (infixl \<open><=\<close> 50) and
+ mem (infixl \<open>:\<close> 50) and
+ not_mem (infixl \<open>~:\<close> 50)
syntax (ASCII)
- "_Ball" :: "[pttrn, i, o] => o" ("(3ALL _:_./ _)" 10)
- "_Bex" :: "[pttrn, i, o] => o" ("(3EX _:_./ _)" 10)
- "_Collect" :: "[pttrn, i, o] => i" ("(1{_: _ ./ _})")
- "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
- "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _: _})" [51,0,51])
- "_UNION" :: "[pttrn, i, i] => i" ("(3UN _:_./ _)" 10)
- "_INTER" :: "[pttrn, i, i] => i" ("(3INT _:_./ _)" 10)
- "_PROD" :: "[pttrn, i, i] => i" ("(3PROD _:_./ _)" 10)
- "_SUM" :: "[pttrn, i, i] => i" ("(3SUM _:_./ _)" 10)
- "_lam" :: "[pttrn, i, i] => i" ("(3lam _:_./ _)" 10)
- "_Tuple" :: "[i, is] => i" ("<(_,/ _)>")
- "_pattern" :: "patterns => pttrn" ("<_>")
+ "_Ball" :: "[pttrn, i, o] => o" (\<open>(3ALL _:_./ _)\<close> 10)
+ "_Bex" :: "[pttrn, i, o] => o" (\<open>(3EX _:_./ _)\<close> 10)
+ "_Collect" :: "[pttrn, i, o] => i" (\<open>(1{_: _ ./ _})\<close>)
+ "_Replace" :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>)
+ "_RepFun" :: "[i, pttrn, i] => i" (\<open>(1{_ ./ _: _})\<close> [51,0,51])
+ "_UNION" :: "[pttrn, i, i] => i" (\<open>(3UN _:_./ _)\<close> 10)
+ "_INTER" :: "[pttrn, i, i] => i" (\<open>(3INT _:_./ _)\<close> 10)
+ "_PROD" :: "[pttrn, i, i] => i" (\<open>(3PROD _:_./ _)\<close> 10)
+ "_SUM" :: "[pttrn, i, i] => i" (\<open>(3SUM _:_./ _)\<close> 10)
+ "_lam" :: "[pttrn, i, i] => i" (\<open>(3lam _:_./ _)\<close> 10)
+ "_Tuple" :: "[i, is] => i" (\<open><(_,/ _)>\<close>)
+ "_pattern" :: "patterns => pttrn" (\<open><_>\<close>)
subsection \<open>Substitution\<close>
--- a/src/ZF/ex/Group.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Group.thy Thu Jan 03 21:15:52 2019 +0100
@@ -22,11 +22,11 @@
"carrier(M) == fst(M)"
definition
- mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70) where
+ mmult :: "[i, i, i] => i" (infixl \<open>\<cdot>\<index>\<close> 70) where
"mmult(M,x,y) == fst(snd(M)) ` <x,y>"
definition
- one :: "i => i" ("\<one>\<index>") where
+ one :: "i => i" (\<open>\<one>\<index>\<close>) where
"one(M) == fst(snd(snd(M)))"
definition
@@ -34,7 +34,7 @@
"update_carrier(M,A) == <A,snd(M)>"
definition
- m_inv :: "i => i => i" ("inv\<index> _" [81] 80) where
+ m_inv :: "i => i => i" (\<open>inv\<index> _\<close> [81] 80) where
"inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
locale monoid = fixes G (structure)
@@ -302,7 +302,7 @@
subsection \<open>Direct Products\<close>
definition
- DirProdGroup :: "[i,i] => i" (infixr "\<Otimes>" 80) where
+ DirProdGroup :: "[i,i] => i" (infixr \<open>\<Otimes>\<close> 80) where
"G \<Otimes> H == <carrier(G) \<times> carrier(H),
(\<lambda><<g,h>, <g', h'>>
\<in> (carrier(G) \<times> carrier(H)) \<times> (carrier(G) \<times> carrier(H)).
@@ -370,7 +370,7 @@
subsection \<open>Isomorphisms\<close>
definition
- iso :: "[i,i] => i" (infixr "\<cong>" 60) where
+ iso :: "[i,i] => i" (infixr \<open>\<cong>\<close> 60) where
"G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
lemma (in group) iso_refl: "id(carrier(G)) \<in> G \<cong> G"
@@ -576,23 +576,23 @@
subsection\<open>Cosets and Quotient Groups\<close>
definition
- r_coset :: "[i,i,i] => i" (infixl "#>\<index>" 60) where
+ r_coset :: "[i,i,i] => i" (infixl \<open>#>\<index>\<close> 60) where
"H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
definition
- l_coset :: "[i,i,i] => i" (infixl "<#\<index>" 60) where
+ l_coset :: "[i,i,i] => i" (infixl \<open><#\<index>\<close> 60) where
"a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
definition
- RCOSETS :: "[i,i] => i" ("rcosets\<index> _" [81] 80) where
+ RCOSETS :: "[i,i] => i" (\<open>rcosets\<index> _\<close> [81] 80) where
"rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
definition
- set_mult :: "[i,i,i] => i" (infixl "<#>\<index>" 60) where
+ set_mult :: "[i,i,i] => i" (infixl \<open><#>\<index>\<close> 60) where
"H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
definition
- SET_INV :: "[i,i] => i" ("set'_inv\<index> _" [81] 80) where
+ SET_INV :: "[i,i] => i" (\<open>set'_inv\<index> _\<close> [81] 80) where
"set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
@@ -600,7 +600,7 @@
assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
notation
- normal (infixl "\<lhd>" 60)
+ normal (infixl \<open>\<lhd>\<close> 60)
subsection \<open>Basic Properties of Cosets\<close>
@@ -860,7 +860,7 @@
subsubsection\<open>Two distinct right cosets are disjoint\<close>
definition
- r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60) where
+ r_congruent :: "[i,i] => i" (\<open>rcong\<index> _\<close> [60] 60) where
"rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
@@ -1020,7 +1020,7 @@
subsection \<open>Quotient Groups: Factorization of a Group\<close>
definition
- FactGroup :: "[i,i] => i" (infixl "Mod" 65) where
+ FactGroup :: "[i,i] => i" (infixl \<open>Mod\<close> 65) where
\<comment> \<open>Actually defined for groups rather than monoids\<close>
"G Mod H ==
<rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
--- a/src/ZF/ex/Primes.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Primes.thy Thu Jan 03 21:15:52 2019 +0100
@@ -8,7 +8,7 @@
theory Primes imports ZF begin
definition
- divides :: "[i,i]=>o" (infixl "dvd" 50) where
+ divides :: "[i,i]=>o" (infixl \<open>dvd\<close> 50) where
"m dvd n == m \<in> nat & n \<in> nat & (\<exists>k \<in> nat. n = m#*k)"
definition
--- a/src/ZF/ex/Ring.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/ex/Ring.thy Thu Jan 03 21:15:52 2019 +0100
@@ -7,8 +7,8 @@
theory Ring imports Group begin
no_notation
- cadd (infixl "\<oplus>" 65) and
- cmult (infixl "\<otimes>" 70)
+ cadd (infixl \<open>\<oplus>\<close> 65) and
+ cmult (infixl \<open>\<otimes>\<close> 70)
(*First, we must simulate a record declaration:
record ring = monoid +
@@ -21,11 +21,11 @@
"add_field(M) = fst(snd(snd(snd(M))))"
definition
- ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65) where
+ ring_add :: "[i, i, i] => i" (infixl \<open>\<oplus>\<index>\<close> 65) where
"ring_add(M,x,y) = add_field(M) ` <x,y>"
definition
- zero :: "i => i" ("\<zero>\<index>") where
+ zero :: "i => i" (\<open>\<zero>\<index>\<close>) where
"zero(M) = fst(snd(snd(snd(snd(M)))))"
@@ -42,11 +42,11 @@
text \<open>Derived operations.\<close>
definition
- a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80) where
+ a_inv :: "[i,i] => i" (\<open>\<ominus>\<index> _\<close> [81] 80) where
"a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
definition
- minus :: "[i,i,i] => i" ("(_ \<ominus>\<index> _)" [65,66] 65) where
+ minus :: "[i,i,i] => i" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65) where
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
locale abelian_monoid = fixes G (structure)
--- a/src/ZF/func.thy Thu Jan 03 21:06:39 2019 +0100
+++ b/src/ZF/func.thy Thu Jan 03 21:15:52 2019 +0100
@@ -451,10 +451,10 @@
(* Let expressions *)
- "_updbind" :: "[i, i] => updbind" ("(2_ :=/ _)")
- "" :: "updbind => updbinds" ("_")
- "_updbinds" :: "[updbind, updbinds] => updbinds" ("_,/ _")
- "_Update" :: "[i, updbinds] => i" ("_/'((_)')" [900,0] 900)
+ "_updbind" :: "[i, i] => updbind" (\<open>(2_ :=/ _)\<close>)
+ "" :: "updbind => updbinds" (\<open>_\<close>)
+ "_updbinds" :: "[updbind, updbinds] => updbinds" (\<open>_,/ _\<close>)
+ "_Update" :: "[i, updbinds] => i" (\<open>_/'((_)')\<close> [900,0] 900)
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"