standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
--- a/src/HOL/Archimedean_Field.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Archimedean_Field.thy Mon Sep 23 13:32:38 2024 +0200
@@ -205,7 +205,7 @@
subsection \<open>Floor function\<close>
class floor_ceiling = archimedean_field +
- fixes floor :: "'a \<Rightarrow> int" ("\<lfloor>_\<rfloor>")
+ fixes floor :: "'a \<Rightarrow> int" (\<open>\<lfloor>_\<rfloor>\<close>)
assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"
lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
@@ -427,7 +427,7 @@
subsection \<open>Ceiling function\<close>
-definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" ("\<lceil>_\<rceil>")
+definition ceiling :: "'a::floor_ceiling \<Rightarrow> int" (\<open>\<lceil>_\<rceil>\<close>)
where "\<lceil>x\<rceil> = - \<lfloor>- x\<rfloor>"
lemma ceiling_correct: "of_int \<lceil>x\<rceil> - 1 < x \<and> x \<le> of_int \<lceil>x\<rceil>"
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Sep 23 13:32:38 2024 +0200
@@ -139,7 +139,7 @@
subsection \<open>Binary sum\<close>
-definition csum (infixr "+c" 65)
+definition csum (infixr \<open>+c\<close> 65)
where "r1 +c r2 \<equiv> |Field r1 <+> Field r2|"
lemma Field_csum: "Field (r +c s) = Inl ` Field r \<union> Inr ` Field s"
@@ -273,7 +273,7 @@
(* Similar setup to the one for SIGMA from theory Big_Operators: *)
syntax "_Csum" ::
"pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set"
- ("(3CSUM _:_. _)" [0, 51, 10] 10)
+ (\<open>(3CSUM _:_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_Csum" == Csum
@@ -291,7 +291,7 @@
subsection \<open>Product\<close>
-definition cprod (infixr "*c" 80) where
+definition cprod (infixr \<open>*c\<close> 80) where
"r1 *c r2 = |Field r1 \<times> Field r2|"
lemma card_order_cprod:
@@ -450,7 +450,7 @@
subsection \<open>Exponentiation\<close>
-definition cexp (infixr "^c" 90) where
+definition cexp (infixr \<open>^c\<close> 90) where
"r1 ^c r2 \<equiv> |Func (Field r2) (Field r1)|"
lemma Card_order_cexp: "Card_order (r1 ^c r2)"
--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Mon Sep 23 13:32:38 2024 +0200
@@ -117,7 +117,7 @@
We shall prove that this notion is unique up to order isomorphism, meaning
that order isomorphism shall be the true identity of cardinals.\<close>
-definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
+definition card_of :: "'a set \<Rightarrow> 'a rel" (\<open>|_|\<close> )
where "card_of A = (SOME r. card_order_on A r)"
lemma card_of_card_order_on: "card_order_on A |A|"
--- a/src/HOL/BNF_Def.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Def.thy Mon Sep 23 13:32:38 2024 +0200
@@ -84,7 +84,7 @@
lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (simp add: collect_def)
-definition convol ("\<langle>(_,/ _)\<rangle>") where
+definition convol (\<open>\<langle>(_,/ _)\<rangle>\<close>) where
"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
lemma fst_convol: "fst \<circ> \<langle>f, g\<rangle> = f"
--- a/src/HOL/BNF_Wellorder_Constructions.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Mon Sep 23 13:32:38 2024 +0200
@@ -334,24 +334,24 @@
where
"ordLeq = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embed r r' f)}"
-abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<=o" 50)
+abbreviation ordLeq2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix \<open><=o\<close> 50)
where "r <=o r' \<equiv> (r,r') \<in> ordLeq"
-abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "\<le>o" 50)
+abbreviation ordLeq3 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix \<open>\<le>o\<close> 50)
where "r \<le>o r' \<equiv> r <=o r'"
definition ordLess :: "('a rel * 'a' rel) set"
where
"ordLess = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. embedS r r' f)}"
-abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "<o" 50)
+abbreviation ordLess2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix \<open><o\<close> 50)
where "r <o r' \<equiv> (r,r') \<in> ordLess"
definition ordIso :: "('a rel * 'a' rel) set"
where
"ordIso = {(r,r'). Well_order r \<and> Well_order r' \<and> (\<exists>f. iso r r' f)}"
-abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix "=o" 50)
+abbreviation ordIso2 :: "'a rel \<Rightarrow> 'a' rel \<Rightarrow> bool" (infix \<open>=o\<close> 50)
where "r =o r' \<equiv> (r,r') \<in> ordIso"
lemmas ordRels_def = ordLeq_def ordLess_def ordIso_def
--- a/src/HOL/Binomial.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Binomial.thy Mon Sep 23 13:32:38 2024 +0200
@@ -18,7 +18,7 @@
text \<open>Combinatorial definition\<close>
-definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infix "choose" 64)
+definition binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infix \<open>choose\<close> 64)
where "n choose k = card {K\<in>Pow {0..<n}. card K = k}"
lemma binomial_right_mono:
@@ -362,7 +362,7 @@
subsection \<open>Generalized binomial coefficients\<close>
-definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infix "gchoose" 64)
+definition gbinomial :: "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a" (infix \<open>gchoose\<close> 64)
where gbinomial_prod_rev: "a gchoose k = prod (\<lambda>i. a - of_nat i) {0..<k} div fact k"
lemma gbinomial_0 [simp]:
--- a/src/HOL/Code_Evaluation.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Code_Evaluation.thy Mon Sep 23 13:32:38 2024 +0200
@@ -55,8 +55,8 @@
bundle term_syntax
begin
-notation App (infixl "<\<cdot>>" 70)
- and valapp (infixl "{\<cdot>}" 70)
+notation App (infixl \<open><\<cdot>>\<close> 70)
+ and valapp (infixl \<open>{\<cdot>}\<close> 70)
end
--- a/src/HOL/Complete_Lattices.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Complete_Lattices.thy Mon Sep 23 13:32:38 2024 +0200
@@ -15,22 +15,22 @@
subsection \<open>Syntactic infimum and supremum operations\<close>
class Inf =
- fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter> _" [900] 900)
+ fixes Inf :: "'a set \<Rightarrow> 'a" (\<open>\<Sqinter> _\<close> [900] 900)
class Sup =
- fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion> _" [900] 900)
+ fixes Sup :: "'a set \<Rightarrow> 'a" (\<open>\<Squnion> _\<close> [900] 900)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _\<in>_./ _)" [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3INF _./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3INF _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3SUP _./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3SUP _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_INF1" "_INF" \<rightleftharpoons> Inf and
@@ -775,7 +775,7 @@
subsubsection \<open>Inter\<close>
-abbreviation Inter :: "'a set set \<Rightarrow> 'a set" ("\<Inter>")
+abbreviation Inter :: "'a set set \<Rightarrow> 'a set" (\<open>\<Inter>\<close>)
where "\<Inter>S \<equiv> \<Sqinter>S"
lemma Inter_eq: "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
@@ -843,16 +843,16 @@
subsubsection \<open>Intersections of families\<close>
syntax (ASCII)
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _./ _)" [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3INT _./ _)\<close> [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3INT _:_./ _)\<close> [0, 0, 10] 10)
syntax
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>_./ _)\<close> [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
- "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" ("(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+ "_INTER1" :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
+ "_INTER" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)\<close> [0, 0, 10] 10)
syntax_consts
"_INTER1" "_INTER" \<rightleftharpoons> Inter
@@ -932,7 +932,7 @@
subsubsection \<open>Union\<close>
-abbreviation Union :: "'a set set \<Rightarrow> 'a set" ("\<Union>")
+abbreviation Union :: "'a set set \<Rightarrow> 'a set" (\<open>\<Union>\<close>)
where "\<Union>S \<equiv> \<Squnion>S"
lemma Union_eq: "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
@@ -1009,16 +1009,16 @@
subsubsection \<open>Unions of families\<close>
syntax (ASCII)
- "_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3UN _./ _)\<close> [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(3UN _:_./ _)\<close> [0, 0, 10] 10)
syntax
- "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3\<Union>_./ _)\<close> [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(3\<Union>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
- "_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+ "_UNION1" :: "pttrns => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<^esub>)/ _)\<close> [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>\<^bsub>_\<in>_\<^esub>)/ _)\<close> [0, 0, 10] 10)
syntax_consts
"_UNION1" "_UNION" \<rightleftharpoons> Union
--- a/src/HOL/Complex.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Complex.thy Mon Sep 23 13:32:38 2024 +0200
@@ -238,7 +238,7 @@
subsection \<open>The Complex Number $i$\<close>
-primcorec imaginary_unit :: complex ("\<i>")
+primcorec imaginary_unit :: complex (\<open>\<i>\<close>)
where
"Re \<i> = 0"
| "Im \<i> = 1"
--- a/src/HOL/Deriv.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Deriv.thy Mon Sep 23 13:32:38 2024 +0200
@@ -14,7 +14,7 @@
subsection \<open>Frechet derivative\<close>
definition has_derivative :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow>
- ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool" (infix "(has'_derivative)" 50)
+ ('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> bool" (infix \<open>(has'_derivative)\<close> 50)
where "(f has_derivative f') F \<longleftrightarrow>
bounded_linear f' \<and>
((\<lambda>y. ((f y - f (Lim F (\<lambda>x. x))) - f' (y - Lim F (\<lambda>x. x))) /\<^sub>R norm (y - Lim F (\<lambda>x. x))) \<longlongrightarrow> 0) F"
@@ -37,14 +37,14 @@
by simp
definition has_field_derivative :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a filter \<Rightarrow> bool"
- (infix "(has'_field'_derivative)" 50)
+ (infix \<open>(has'_field'_derivative)\<close> 50)
where "(f has_field_derivative D) F \<longleftrightarrow> (f has_derivative (*) D) F"
lemma DERIV_cong: "(f has_field_derivative X) F \<Longrightarrow> X = Y \<Longrightarrow> (f has_field_derivative Y) F"
by simp
definition has_vector_derivative :: "(real \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> real filter \<Rightarrow> bool"
- (infix "has'_vector'_derivative" 50)
+ (infix \<open>has'_vector'_derivative\<close> 50)
where "(f has_vector_derivative f') net \<longleftrightarrow> (f has_derivative (\<lambda>x. x *\<^sub>R f')) net"
lemma has_vector_derivative_eq_rhs:
@@ -70,7 +70,7 @@
\<close>
abbreviation (input)
FDERIV :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- ("(FDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+ (\<open>(FDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where "FDERIV f x :> f' \<equiv> (f has_derivative f') (at x)"
lemma has_derivative_bounded_linear: "(f has_derivative f') F \<Longrightarrow> bounded_linear f'"
@@ -665,7 +665,7 @@
subsection \<open>Differentiability predicate\<close>
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a filter \<Rightarrow> bool"
- (infix "differentiable" 50)
+ (infix \<open>differentiable\<close> 50)
where "f differentiable F \<longleftrightarrow> (\<exists>D. (f has_derivative D) F)"
lemma differentiable_subset:
@@ -782,11 +782,11 @@
abbreviation (input)
DERIV :: "('a::real_normed_field \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
- ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
+ (\<open>(DERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where "DERIV f x :> D \<equiv> (f has_field_derivative D) (at x)"
abbreviation has_real_derivative :: "(real \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> real filter \<Rightarrow> bool"
- (infix "(has'_real'_derivative)" 50)
+ (infix \<open>(has'_real'_derivative)\<close> 50)
where "(f has_real_derivative D) F \<equiv> (f has_field_derivative D) F"
lemma real_differentiable_def:
--- a/src/HOL/Enum.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Enum.thy Mon Sep 23 13:32:38 2024 +0200
@@ -497,7 +497,7 @@
datatype (plugins only: code "quickcheck" extraction) finite_1 =
a\<^sub>1
-notation (output) a\<^sub>1 ("a\<^sub>1")
+notation (output) a\<^sub>1 (\<open>a\<^sub>1\<close>)
lemma UNIV_finite_1:
"UNIV = {a\<^sub>1}"
@@ -601,8 +601,8 @@
datatype (plugins only: code "quickcheck" extraction) finite_2 =
a\<^sub>1 | a\<^sub>2
-notation (output) a\<^sub>1 ("a\<^sub>1")
-notation (output) a\<^sub>2 ("a\<^sub>2")
+notation (output) a\<^sub>1 (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2 (\<open>a\<^sub>2\<close>)
lemma UNIV_finite_2:
"UNIV = {a\<^sub>1, a\<^sub>2}"
@@ -730,9 +730,9 @@
datatype (plugins only: code "quickcheck" extraction) finite_3 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3
-notation (output) a\<^sub>1 ("a\<^sub>1")
-notation (output) a\<^sub>2 ("a\<^sub>2")
-notation (output) a\<^sub>3 ("a\<^sub>3")
+notation (output) a\<^sub>1 (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2 (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3 (\<open>a\<^sub>3\<close>)
lemma UNIV_finite_3:
"UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3}"
@@ -971,10 +971,10 @@
datatype (plugins only: code "quickcheck" extraction) finite_4 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
-notation (output) a\<^sub>1 ("a\<^sub>1")
-notation (output) a\<^sub>2 ("a\<^sub>2")
-notation (output) a\<^sub>3 ("a\<^sub>3")
-notation (output) a\<^sub>4 ("a\<^sub>4")
+notation (output) a\<^sub>1 (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2 (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3 (\<open>a\<^sub>3\<close>)
+notation (output) a\<^sub>4 (\<open>a\<^sub>4\<close>)
lemma UNIV_finite_4:
"UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4}"
@@ -1060,11 +1060,11 @@
datatype (plugins only: code "quickcheck" extraction) finite_5 =
a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
-notation (output) a\<^sub>1 ("a\<^sub>1")
-notation (output) a\<^sub>2 ("a\<^sub>2")
-notation (output) a\<^sub>3 ("a\<^sub>3")
-notation (output) a\<^sub>4 ("a\<^sub>4")
-notation (output) a\<^sub>5 ("a\<^sub>5")
+notation (output) a\<^sub>1 (\<open>a\<^sub>1\<close>)
+notation (output) a\<^sub>2 (\<open>a\<^sub>2\<close>)
+notation (output) a\<^sub>3 (\<open>a\<^sub>3\<close>)
+notation (output) a\<^sub>4 (\<open>a\<^sub>4\<close>)
+notation (output) a\<^sub>5 (\<open>a\<^sub>5\<close>)
lemma UNIV_finite_5:
"UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"
--- a/src/HOL/Equiv_Relations.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Equiv_Relations.thy Mon Sep 23 13:32:38 2024 +0200
@@ -88,7 +88,7 @@
subsection \<open>Quotients\<close>
-definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl "'/'/" 90)
+definition quotient :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set" (infixl \<open>'/'/\<close> 90)
where "A//r = (\<Union>x \<in> A. {r``{x}})" \<comment> \<open>set of equiv classes\<close>
lemma quotientI: "x \<in> A \<Longrightarrow> r``{x} \<in> A//r"
@@ -180,7 +180,7 @@
lemma congruentD: "congruent r f \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> f y = f z"
by (auto simp add: congruent_def)
-abbreviation RESPECTS :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects" 80)
+abbreviation RESPECTS :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr \<open>respects\<close> 80)
where "f respects r \<equiv> congruent r f"
@@ -247,7 +247,7 @@
by (auto simp add: congruent2_def)
text \<open>Abbreviation for the common case where the relations are identical.\<close>
-abbreviation RESPECTS2:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr "respects2" 80)
+abbreviation RESPECTS2:: "('a \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" (infixr \<open>respects2\<close> 80)
where "f respects2 r \<equiv> congruent2 r r f"
--- a/src/HOL/Fields.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Fields.thy Mon Sep 23 13:32:38 2024 +0200
@@ -23,7 +23,7 @@
fixes inverse :: "'a \<Rightarrow> 'a"
begin
-abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>'/\<close> 70)
where
"inverse_divide \<equiv> divide"
--- a/src/HOL/Filter.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Filter.thy Mon Sep 23 13:32:38 2024 +0200
@@ -40,7 +40,7 @@
where "eventually P F \<longleftrightarrow> Rep_filter F P"
syntax
- "_eventually" :: "pttrn => 'a filter => bool => bool" ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+ "_eventually" :: "pttrn => 'a filter => bool => bool" (\<open>(3\<forall>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_eventually" == eventually
translations
@@ -160,7 +160,7 @@
where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
syntax
- "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+ "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>\<^sub>F _ in _./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_frequently" == frequently
translations
@@ -1033,15 +1033,15 @@
definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
-abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>\<^sub>\<infinity>" 10)
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder \<open>\<exists>\<^sub>\<infinity>\<close> 10)
where "Inf_many P \<equiv> frequently P cofinite"
-abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>\<^sub>\<infinity>" 10)
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder \<open>\<forall>\<^sub>\<infinity>\<close> 10)
where "Alm_all P \<equiv> eventually P cofinite"
notation (ASCII)
- Inf_many (binder "INFM " 10) and
- Alm_all (binder "MOST " 10)
+ Inf_many (binder \<open>INFM \<close> 10) and
+ Alm_all (binder \<open>MOST \<close> 10)
lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
unfolding cofinite_def
@@ -1080,7 +1080,7 @@
subsubsection \<open>Product of filters\<close>
-definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
+definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr \<open>\<times>\<^sub>F\<close> 80) where
"prod_filter F G =
(\<Sqinter>(P, Q)\<in>{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
@@ -1307,7 +1307,7 @@
"filterlim f F2 F1 \<longleftrightarrow> filtermap f F1 \<le> F2"
syntax
- "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
+ "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(3LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
syntax_consts
"_LIM" == filterlim
--- a/src/HOL/Fun.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Fun.thy Mon Sep 23 13:32:38 2024 +0200
@@ -45,11 +45,11 @@
subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
-definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>" 55)
+definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl \<open>\<circ>\<close> 55)
where "f \<circ> g = (\<lambda>x. f (g x))"
notation (ASCII)
- comp (infixl "o" 55)
+ comp (infixl \<open>o\<close> 55)
lemma comp_apply [simp]: "(f \<circ> g) x = f (g x)"
by (simp add: comp_def)
@@ -102,7 +102,7 @@
subsection \<open>The Forward Composition Operator \<open>fcomp\<close>\<close>
-definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
+definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl \<open>\<circ>>\<close> 60)
where "f \<circ>> g = (\<lambda>x. g (f x))"
lemma fcomp_apply [simp]: "(f \<circ>> g) x = g (f x)"
@@ -123,7 +123,7 @@
code_printing
constant fcomp \<rightharpoonup> (Eval) infixl 1 "#>"
-no_notation fcomp (infixl "\<circ>>" 60)
+no_notation fcomp (infixl \<open>\<circ>>\<close> 60)
subsection \<open>Mapping functions\<close>
@@ -841,10 +841,10 @@
nonterminal updbinds and updbind
syntax
- "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" ("(2_ :=/ _)")
- "" :: "updbind \<Rightarrow> updbinds" ("_")
- "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
- "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" ("_/'((_)')" [1000, 0] 900)
+ "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
+ "" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
+ "_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
+ "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" (\<open>_/'((_)')\<close> [1000, 0] 900)
syntax_consts
"_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
--- a/src/HOL/GCD.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/GCD.thy Mon Sep 23 13:32:38 2024 +0200
@@ -37,7 +37,7 @@
subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
locale bounded_quasi_semilattice = abel_semigroup +
- fixes top :: 'a ("\<^bold>\<top>") and bot :: 'a ("\<^bold>\<bottom>")
+ fixes top :: 'a (\<open>\<^bold>\<top>\<close>) and bot :: 'a (\<open>\<^bold>\<bottom>\<close>)
and normalize :: "'a \<Rightarrow> 'a"
assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
@@ -148,10 +148,10 @@
and Lcm :: "'a set \<Rightarrow> 'a"
syntax
- "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _./ _)" [0, 10] 10)
- "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3GCD _\<in>_./ _)" [0, 0, 10] 10)
- "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _./ _)" [0, 10] 10)
- "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3LCM _\<in>_./ _)" [0, 0, 10] 10)
+ "_GCD1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _./ _)\<close> [0, 10] 10)
+ "_GCD" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3GCD _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_LCM1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _./ _)\<close> [0, 10] 10)
+ "_LCM" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3LCM _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_GCD1" "_GCD" \<rightleftharpoons> Gcd and
@@ -1067,14 +1067,14 @@
sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
defines
- Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+ Gcd_fin (\<open>Gcd\<^sub>f\<^sub>i\<^sub>n\<close>) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
defines
- Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
+ Lcm_fin (\<open>Lcm\<^sub>f\<^sub>i\<^sub>n\<close>) = Lcm_fin.F ..
abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
@@ -2851,7 +2851,7 @@
definition (in semiring_1) semiring_char :: "'a itself \<Rightarrow> nat"
where "semiring_char _ = Gcd {n. of_nat n = (0 :: 'a)}"
-syntax "_type_char" :: "type => nat" ("(1CHAR/(1'(_')))")
+syntax "_type_char" :: "type => nat" (\<open>(1CHAR/(1'(_')))\<close>)
syntax_consts "_type_char" \<rightleftharpoons> semiring_char
translations "CHAR('t)" \<rightharpoonup> "CONST semiring_char (CONST Pure.type :: 't itself)"
print_translation \<open>
--- a/src/HOL/Groups.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Groups.thy Mon Sep 23 13:32:38 2024 +0200
@@ -50,7 +50,7 @@
\<close>
locale semigroup =
- fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^bold>*" 70)
+ fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>\<^bold>*\<close> 70)
assumes assoc [ac_simps]: "a \<^bold>* b \<^bold>* c = a \<^bold>* (b \<^bold>* c)"
locale abel_semigroup = semigroup +
@@ -68,12 +68,12 @@
end
locale monoid = semigroup +
- fixes z :: 'a ("\<^bold>1")
+ fixes z :: 'a (\<open>\<^bold>1\<close>)
assumes left_neutral [simp]: "\<^bold>1 \<^bold>* a = a"
assumes right_neutral [simp]: "a \<^bold>* \<^bold>1 = a"
locale comm_monoid = abel_semigroup +
- fixes z :: 'a ("\<^bold>1")
+ fixes z :: 'a (\<open>\<^bold>1\<close>)
assumes comm_neutral: "a \<^bold>* \<^bold>1 = a"
begin
@@ -83,7 +83,7 @@
end
locale group = semigroup +
- fixes z :: 'a ("\<^bold>1")
+ fixes z :: 'a (\<open>\<^bold>1\<close>)
fixes inverse :: "'a \<Rightarrow> 'a"
assumes group_left_neutral: "\<^bold>1 \<^bold>* a = a"
assumes left_inverse [simp]: "inverse a \<^bold>* a = \<^bold>1"
@@ -158,10 +158,10 @@
subsection \<open>Generic operations\<close>
class zero =
- fixes zero :: 'a ("0")
+ fixes zero :: 'a (\<open>0\<close>)
class one =
- fixes one :: 'a ("1")
+ fixes one :: 'a (\<open>1\<close>)
hide_const (open) zero one
@@ -192,16 +192,16 @@
\<close> \<comment> \<open>show types that are presumably too general\<close>
class plus =
- fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
+ fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>+\<close> 65)
class minus =
- fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
+ fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>-\<close> 65)
class uminus =
- fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
+ fixes uminus :: "'a \<Rightarrow> 'a" (\<open>- _\<close> [81] 80)
class times =
- fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
+ fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>*\<close> 70)
subsection \<open>Semigroups and Monoids\<close>
@@ -1164,7 +1164,7 @@
end
class abs =
- fixes abs :: "'a \<Rightarrow> 'a" ("\<bar>_\<bar>")
+ fixes abs :: "'a \<Rightarrow> 'a" (\<open>\<bar>_\<bar>\<close>)
class sgn =
fixes sgn :: "'a \<Rightarrow> 'a"
--- a/src/HOL/Groups_Big.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Groups_Big.thy Mon Sep 23 13:32:38 2024 +0200
@@ -643,7 +643,7 @@
sublocale sum: comm_monoid_set plus 0
defines sum = sum.F and sum' = sum.G ..
-abbreviation Sum ("\<Sum>")
+abbreviation Sum (\<open>\<Sum>\<close>)
where "\<Sum> \<equiv> sum (\<lambda>x. x)"
end
@@ -651,9 +651,9 @@
text \<open>Now: lots of fancy syntax. First, \<^term>\<open>sum (\<lambda>x. e) A\<close> is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
syntax (ASCII)
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(3SUM (_/:_)./ _)" [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(3SUM (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" ("(2\<Sum>(_/\<in>_)./ _)" [0, 51, 10] 10)
+ "_sum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add" (\<open>(2\<Sum>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum" \<rightleftharpoons> sum
@@ -665,9 +665,9 @@
text \<open>Instead of \<^term>\<open>\<Sum>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
syntax (ASCII)
- "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
+ "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3SUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
+ "_qsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qsum" == sum
@@ -1415,15 +1415,15 @@
sublocale prod: comm_monoid_set times 1
defines prod = prod.F and prod' = prod.G ..
-abbreviation Prod ("\<Prod>_" [1000] 999)
+abbreviation Prod (\<open>\<Prod>_\<close> [1000] 999)
where "\<Prod>A \<equiv> prod (\<lambda>x. x) A"
end
syntax (ASCII)
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(4PROD (_/:_)./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(4PROD (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" ("(2\<Prod>(_/\<in>_)./ _)" [0, 51, 10] 10)
+ "_prod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult" (\<open>(2\<Prod>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod" == prod
@@ -1435,9 +1435,9 @@
text \<open>Instead of \<^term>\<open>\<Prod>x\<in>{x. P}. e\<close> we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
syntax (ASCII)
- "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(4PROD _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
+ "_qprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Prod>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qprod" == prod
--- a/src/HOL/Groups_List.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Groups_List.thy Mon Sep 23 13:32:38 2024 +0200
@@ -98,9 +98,9 @@
text \<open>Some syntactic sugar for summing a function over a list:\<close>
syntax (ASCII)
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3SUM _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_sum_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
+ "_sum_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Sum>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_sum_list" == sum_list
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -597,9 +597,9 @@
text \<open>Some syntactic sugar:\<close>
syntax (ASCII)
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3PROD _<-_. _)" [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3PROD _<-_. _)\<close> [0, 51, 10] 10)
syntax
- "_prod_list" :: "pttrn => 'a list => 'b => 'b" ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
+ "_prod_list" :: "pttrn => 'a list => 'b => 'b" (\<open>(3\<Prod>_\<leftarrow>_. _)\<close> [0, 51, 10] 10)
syntax_consts
"_prod_list" \<rightleftharpoons> prod_list
translations \<comment> \<open>Beware of argument permutation!\<close>
--- a/src/HOL/HOL.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/HOL.thy Mon Sep 23 13:32:38 2024 +0200
@@ -81,16 +81,16 @@
typedecl bool
-judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5)
-
-axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25)
+judgment Trueprop :: "bool \<Rightarrow> prop" (\<open>(_)\<close> 5)
+
+axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<longrightarrow>\<close> 25)
and eq :: "['a, 'a] \<Rightarrow> bool"
and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
notation (input)
- eq (infixl "=" 50)
+ eq (infixl \<open>=\<close> 50)
notation (output)
- eq (infix "=" 50)
+ eq (infix \<open>=\<close> 50)
text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax
because of the large amount of material that relies on infixl.\<close>
@@ -100,22 +100,22 @@
definition True :: bool
where "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
-definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<forall>" 10)
+definition All :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder \<open>\<forall>\<close> 10)
where "All P \<equiv> (P = (\<lambda>x. True))"
-definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "\<exists>" 10)
+definition Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder \<open>\<exists>\<close> 10)
where "Ex P \<equiv> \<forall>Q. (\<forall>x. P x \<longrightarrow> Q) \<longrightarrow> Q"
definition False :: bool
where "False \<equiv> (\<forall>P. P)"
-definition Not :: "bool \<Rightarrow> bool" ("\<not> _" [40] 40)
+definition Not :: "bool \<Rightarrow> bool" (\<open>\<not> _\<close> [40] 40)
where not_def: "\<not> P \<equiv> P \<longrightarrow> False"
-definition conj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<and>" 35)
+definition conj :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<and>\<close> 35)
where and_def: "P \<and> Q \<equiv> \<forall>R. (P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> R"
-definition disj :: "[bool, bool] \<Rightarrow> bool" (infixr "\<or>" 30)
+definition disj :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<or>\<close> 30)
where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
definition Uniq :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -127,8 +127,8 @@
subsubsection \<open>Additional concrete syntax\<close>
-syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(4?< _./ _)" [0, 10] 10)
-syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)" [0, 10] 10)
+syntax (ASCII) "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(4?< _./ _)\<close> [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
syntax_consts "_Uniq" \<rightleftharpoons> Uniq
@@ -140,10 +140,10 @@
syntax (ASCII)
- "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! _./ _)" [0, 10] 10)
+ "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX! _./ _)\<close> [0, 10] 10)
syntax (input)
- "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3?! _./ _)" [0, 10] 10)
-syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!_./ _)" [0, 10] 10)
+ "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3?! _./ _)\<close> [0, 10] 10)
+syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>!_./ _)\<close> [0, 10] 10)
syntax_consts "_Ex1" \<rightleftharpoons> Ex1
@@ -155,8 +155,8 @@
syntax
- "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>_./ _)" [0, 10] 10)
- "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" ("(3\<nexists>!_./ _)" [0, 10] 10)
+ "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<nexists>_./ _)\<close> [0, 10] 10)
+ "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<nexists>!_./ _)\<close> [0, 10] 10)
syntax_consts
"_Not_Ex" \<rightleftharpoons> Ex and
"_Not_Ex1" \<rightleftharpoons> Ex1
@@ -165,21 +165,21 @@
"\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
-abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix "\<noteq>" 50)
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix \<open>\<noteq>\<close> 50)
where "x \<noteq> y \<equiv> \<not> (x = y)"
notation (ASCII)
- Not ("~ _" [40] 40) and
- conj (infixr "&" 35) and
- disj (infixr "|" 30) and
- implies (infixr "-->" 25) and
- not_equal (infix "~=" 50)
+ Not (\<open>~ _\<close> [40] 40) and
+ conj (infixr \<open>&\<close> 35) and
+ disj (infixr \<open>|\<close> 30) and
+ implies (infixr \<open>-->\<close> 25) and
+ not_equal (infix \<open>~=\<close> 50)
abbreviation (iff)
- iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25)
+ iff :: "[bool, bool] \<Rightarrow> bool" (infixr \<open>\<longleftrightarrow>\<close> 25)
where "A \<longleftrightarrow> B \<equiv> A = B"
-syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" ("(3THE _./ _)" [0, 10] 10)
+syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a" (\<open>(3THE _./ _)\<close> [0, 10] 10)
syntax_consts "_The" \<rightleftharpoons> The
translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
print_translation \<open>
@@ -190,20 +190,20 @@
nonterminal case_syn and cases_syn
syntax
- "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" ("(case _ of/ _)" 10)
- "_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ \<Rightarrow>/ _)" 10)
- "" :: "case_syn \<Rightarrow> cases_syn" ("_")
- "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn" ("_/ | _")
+ "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" (\<open>(case _ of/ _)\<close> 10)
+ "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+ "" :: "case_syn \<Rightarrow> cases_syn" (\<open>_\<close>)
+ "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn" (\<open>_/ | _\<close>)
syntax (ASCII)
- "_case1" :: "['a, 'b] \<Rightarrow> case_syn" ("(2_ =>/ _)" 10)
+ "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(2_ =>/ _)\<close> 10)
notation (ASCII)
- All (binder "ALL " 10) and
- Ex (binder "EX " 10)
+ All (binder \<open>ALL \<close> 10) and
+ Ex (binder \<open>EX \<close> 10)
notation (input)
- All (binder "! " 10) and
- Ex (binder "? " 10)
+ All (binder \<open>! \<close> 10) and
+ Ex (binder \<open>? \<close> 10)
subsubsection \<open>Axioms and basic definitions\<close>
@@ -224,7 +224,7 @@
True_or_False: "(P = True) \<or> (P = False)"
-definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
+definition If :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(if (_)/ then (_)/ else (_))\<close> [0, 0, 10] 10)
where "If P x y \<equiv> (THE z::'a. (P = True \<longrightarrow> z = x) \<and> (P = False \<longrightarrow> z = y))"
definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
@@ -232,10 +232,10 @@
nonterminal letbinds and letbind
syntax
- "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" ("(2_ =/ _)" 10)
- "" :: "letbind \<Rightarrow> letbinds" ("_")
- "_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" ("(let (_)/ in (_))" [0, 10] 10)
+ "_bind" :: "[pttrn, 'a] \<Rightarrow> letbind" (\<open>(2_ =/ _)\<close> 10)
+ "" :: "letbind \<Rightarrow> letbinds" (\<open>_\<close>)
+ "_binds" :: "[letbind, letbinds] \<Rightarrow> letbinds" (\<open>_;/ _\<close>)
+ "_Let" :: "[letbinds, 'a] \<Rightarrow> 'a" (\<open>(let (_)/ in (_))\<close> [0, 10] 10)
syntax_consts
"_bind" "_binds" "_Let" \<rightleftharpoons> Let
translations
@@ -1177,7 +1177,7 @@
its premise.
\<close>
-definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop" (infixr "=simp=>" 1)
+definition simp_implies :: "prop \<Rightarrow> prop \<Rightarrow> prop" (infixr \<open>=simp=>\<close> 1)
where "simp_implies \<equiv> (\<Longrightarrow>)"
lemma simp_impliesI:
--- a/src/HOL/Hilbert_Choice.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Hilbert_Choice.thy Mon Sep 23 13:32:38 2024 +0200
@@ -17,11 +17,11 @@
where someI: "P x \<Longrightarrow> P (Eps P)"
syntax (epsilon)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3\<some>_./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3\<some>_./ _)\<close> [0, 10] 10)
syntax (input)
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3@ _./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3@ _./ _)\<close> [0, 10] 10)
syntax
- "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" ("(3SOME _./ _)" [0, 10] 10)
+ "_Eps" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3SOME _./ _)\<close> [0, 10] 10)
syntax_consts "_Eps" \<rightleftharpoons> Eps
--- a/src/HOL/Hull.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Hull.thy Mon Sep 23 13:32:38 2024 +0200
@@ -11,7 +11,7 @@
subsection \<open>A generic notion of the convex, affine, conic hull, or closed "hull".\<close>
-definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "hull" 75)
+definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl \<open>hull\<close> 75)
where "S hull s = \<Inter>{t. S t \<and> s \<subseteq> t}"
lemma hull_same: "S s \<Longrightarrow> S hull s = s"
--- a/src/HOL/Inductive.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Inductive.thy Mon Sep 23 13:32:38 2024 +0200
@@ -525,9 +525,9 @@
text \<open>Lambda-abstractions with pattern matching:\<close>
syntax (ASCII)
- "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(%_)" 10)
+ "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(%_)\<close> 10)
syntax
- "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" ("(\<lambda>_)" 10)
+ "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b" (\<open>(\<lambda>_)\<close> 10)
parse_translation \<open>
let
fun fun_tr ctxt [cs] =
--- a/src/HOL/Int.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Int.thy Mon Sep 23 13:32:38 2024 +0200
@@ -911,7 +911,7 @@
context ring_1
begin
-definition Ints :: "'a set" ("\<int>")
+definition Ints :: "'a set" (\<open>\<int>\<close>)
where "\<int> = range of_int"
lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
@@ -1743,7 +1743,7 @@
The notation `powi' is inspired by the `powr' notation for real/complex exponentiation.
\<close>
-definition power_int :: "'a :: {inverse, power} \<Rightarrow> int \<Rightarrow> 'a" (infixr "powi" 80) where
+definition power_int :: "'a :: {inverse, power} \<Rightarrow> int \<Rightarrow> 'a" (infixr \<open>powi\<close> 80) where
"power_int x n = (if n \<ge> 0 then x ^ nat n else inverse x ^ (nat (-n)))"
lemma power_int_0_right [simp]: "power_int x 0 = 1"
--- a/src/HOL/Lattices.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Lattices.thy Mon Sep 23 13:32:38 2024 +0200
@@ -31,8 +31,8 @@
locale semilattice_neutr = semilattice + comm_monoid
locale semilattice_order = semilattice +
- fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
- and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
+ fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>\<^bold>\<le>\<close> 50)
+ and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>\<^bold><\<close> 50)
assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
begin
@@ -165,10 +165,10 @@
subsection \<open>Syntactic infimum and supremum operations\<close>
class inf =
- fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
+ fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>\<sqinter>\<close> 70)
class sup =
- fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+ fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>\<squnion>\<close> 65)
subsection \<open>Concrete lattices\<close>
@@ -616,7 +616,7 @@
subsection \<open>Uniqueness of inf and sup\<close>
lemma (in semilattice_inf) inf_unique:
- fixes f (infixl "\<triangle>" 70)
+ fixes f (infixl \<open>\<triangle>\<close> 70)
assumes le1: "\<And>x y. x \<triangle> y \<le> x"
and le2: "\<And>x y. x \<triangle> y \<le> y"
and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
@@ -631,7 +631,7 @@
qed
lemma (in semilattice_sup) sup_unique:
- fixes f (infixl "\<nabla>" 70)
+ fixes f (infixl \<open>\<nabla>\<close> 70)
assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y"
and ge2: "\<And>x y. y \<le> x \<nabla> y"
and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
--- a/src/HOL/Lattices_Big.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Lattices_Big.thy Mon Sep 23 13:32:38 2024 +0200
@@ -309,7 +309,7 @@
sublocale Inf_fin: semilattice_order_set inf less_eq less
defines
- Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Inf_fin.F ..
+ Inf_fin (\<open>\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _\<close> [900] 900) = Inf_fin.F ..
end
@@ -318,7 +318,7 @@
sublocale Sup_fin: semilattice_order_set sup greater_eq greater
defines
- Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Sup_fin.F ..
+ Sup_fin (\<open>\<Squnion>\<^sub>f\<^sub>i\<^sub>n _\<close> [900] 900) = Sup_fin.F ..
end
@@ -465,10 +465,10 @@
end
syntax
- "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10)
- "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _\<in>_./ _)" [0, 0, 10] 10)
- "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10)
- "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _\<in>_./ _)" [0, 0, 10] 10)
+ "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MIN _./ _)\<close> [0, 10] 10)
+ "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MIN _\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MAX _./ _)\<close> [0, 10] 10)
+ "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3MAX _\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_MIN1" "_MIN" \<rightleftharpoons> Min and
@@ -923,7 +923,7 @@
syntax
"_arg_min" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'b"
- ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10)
+ (\<open>(3ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
"_arg_min" \<rightleftharpoons> arg_min
translations
@@ -1034,7 +1034,7 @@
syntax
"_arg_max" :: "('b \<Rightarrow> 'a) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
- ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10)
+ (\<open>(3ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
"_arg_max" \<rightleftharpoons> arg_max
translations
--- a/src/HOL/List.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/List.thy Mon Sep 23 13:32:38 2024 +0200
@@ -9,8 +9,8 @@
begin
datatype (set: 'a) list =
- Nil ("[]")
- | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+ Nil (\<open>[]\<close>)
+ | Cons (hd: 'a) (tl: "'a list") (infixr \<open>#\<close> 65)
for
map: map
rel: list_all2
@@ -47,9 +47,9 @@
nonterminal list_args
syntax
- "" :: "'a \<Rightarrow> list_args" ("_")
- "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" ("_,/ _")
- "_list" :: "list_args => 'a list" ("[(_)]")
+ "" :: "'a \<Rightarrow> list_args" (\<open>_\<close>)
+ "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args" (\<open>_,/ _\<close>)
+ "_list" :: "list_args => 'a list" (\<open>[(_)]\<close>)
syntax_consts
"_list_args" "_list" == Cons
translations
@@ -72,7 +72,7 @@
definition coset :: "'a list \<Rightarrow> 'a set" where
[simp]: "coset xs = - set xs"
-primrec append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
+primrec append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr \<open>@\<close> 65) where
append_Nil: "[] @ ys = ys" |
append_Cons: "(x#xs) @ ys = x # xs @ ys"
@@ -86,9 +86,9 @@
text \<open>Special input syntax for filter:\<close>
syntax (ASCII)
- "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(1[_<-_./ _])\<close>)
syntax
- "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_\<leftarrow>_ ./ _])")
+ "_filter" :: "[pttrn, 'a list, bool] => 'a list" (\<open>(1[_\<leftarrow>_ ./ _])\<close>)
syntax_consts
"_filter" \<rightleftharpoons> filter
translations
@@ -122,7 +122,7 @@
\<comment> \<open>Warning: simpset does not contain this definition, but separate
theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close>
-primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl "!" 100) where
+primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl \<open>!\<close> 100) where
nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
\<comment> \<open>Warning: simpset does not contain this definition, but separate
theorems for \<open>n = 0\<close> and \<open>n = Suc k\<close>\<close>
@@ -135,10 +135,10 @@
nonterminal lupdbinds and lupdbind
syntax
- "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")
- "" :: "lupdbind => lupdbinds" ("_")
- "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")
- "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [1000,0] 900)
+ "_lupdbind":: "['a, 'a] => lupdbind" (\<open>(2_ :=/ _)\<close>)
+ "" :: "lupdbind => lupdbinds" (\<open>_\<close>)
+ "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" (\<open>_,/ _\<close>)
+ "_LUpdate" :: "['a, lupdbinds] => 'a" (\<open>_/[(_)]\<close> [1000,0] 900)
syntax_consts
"_lupdbind" "_lupdbinds" "_LUpdate" == list_update
@@ -175,7 +175,7 @@
"product_lists [] = [[]]" |
"product_lists (xs # xss) = concat (map (\<lambda>x. map (Cons x) (product_lists xss)) xs)"
-primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
+primrec upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" (\<open>(1[_..</_'])\<close>) where
upt_0: "[i..<0] = []" |
upt_Suc: "[i..<(Suc j)] = (if i \<le> j then [i..<j] @ [j] else [])"
@@ -449,15 +449,15 @@
nonterminal lc_qual and lc_quals
syntax
- "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" ("[_ . __")
- "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
- "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
+ "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" (\<open>[_ . __\<close>)
+ "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" (\<open>_ \<leftarrow> _\<close>)
+ "_lc_test" :: "bool \<Rightarrow> lc_qual" (\<open>_\<close>)
(*"_lc_let" :: "letbinds => lc_qual" ("let _")*)
- "_lc_end" :: "lc_quals" ("]")
- "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
+ "_lc_end" :: "lc_quals" (\<open>]\<close>)
+ "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (\<open>, __\<close>)
syntax (ASCII)
- "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
+ "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" (\<open>_ <- _\<close>)
parse_translation \<open>
let
@@ -2811,7 +2811,7 @@
lemma semilattice_map2:
"semilattice (map2 (\<^bold>*))" if "semilattice (\<^bold>*)"
- for f (infixl "\<^bold>*" 70)
+ for f (infixl \<open>\<^bold>*\<close> 70)
proof -
from that interpret semilattice f .
show ?thesis
@@ -3432,7 +3432,7 @@
subsubsection \<open>\<open>upto\<close>: interval-list on \<^typ>\<open>int\<close>\<close>
-function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
+function upto :: "int \<Rightarrow> int \<Rightarrow> int list" (\<open>(1[_../_])\<close>) where
"upto i j = (if i \<le> j then i # [i+1..j] else [])"
by auto
termination
@@ -6219,7 +6219,7 @@
where "sorted_key_list_of_set f \<equiv> folding_on.F (insort_key f) []"
locale folding_insort_key = lo?: linorder "less_eq :: 'a \<Rightarrow> 'a \<Rightarrow> bool" less
- for less_eq (infix "\<preceq>" 50) and less (infix "\<prec>" 50) +
+ for less_eq (infix \<open>\<preceq>\<close> 50) and less (infix \<open>\<prec>\<close> 50) +
fixes S
fixes f :: "'b \<Rightarrow> 'a"
assumes inj_on: "inj_on f S"
--- a/src/HOL/Main.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Main.thy Mon Sep 23 13:32:38 2024 +0200
@@ -32,28 +32,28 @@
subsection \<open>Syntax cleanup\<close>
no_notation
- ordLeq2 (infix "<=o" 50) and
- ordLeq3 (infix "\<le>o" 50) and
- ordLess2 (infix "<o" 50) and
- ordIso2 (infix "=o" 50) and
- card_of ("|_|") and
- BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
- BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
- BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
- BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
+ ordLeq2 (infix \<open><=o\<close> 50) and
+ ordLeq3 (infix \<open>\<le>o\<close> 50) and
+ ordLess2 (infix \<open><o\<close> 50) and
+ ordIso2 (infix \<open>=o\<close> 50) and
+ card_of (\<open>|_|\<close>) and
+ BNF_Cardinal_Arithmetic.csum (infixr \<open>+c\<close> 65) and
+ BNF_Cardinal_Arithmetic.cprod (infixr \<open>*c\<close> 80) and
+ BNF_Cardinal_Arithmetic.cexp (infixr \<open>^c\<close> 90) and
+ BNF_Def.convol (\<open>\<langle>(_,/ _)\<rangle>\<close>)
bundle cardinal_syntax
begin
notation
- ordLeq2 (infix "<=o" 50) and
- ordLeq3 (infix "\<le>o" 50) and
- ordLess2 (infix "<o" 50) and
- ordIso2 (infix "=o" 50) and
- card_of ("|_|") and
- BNF_Cardinal_Arithmetic.csum (infixr "+c" 65) and
- BNF_Cardinal_Arithmetic.cprod (infixr "*c" 80) and
- BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90)
+ ordLeq2 (infix \<open><=o\<close> 50) and
+ ordLeq3 (infix \<open>\<le>o\<close> 50) and
+ ordLess2 (infix \<open><o\<close> 50) and
+ ordIso2 (infix \<open>=o\<close> 50) and
+ card_of (\<open>|_|\<close>) and
+ BNF_Cardinal_Arithmetic.csum (infixr \<open>+c\<close> 65) and
+ BNF_Cardinal_Arithmetic.cprod (infixr \<open>*c\<close> 80) and
+ BNF_Cardinal_Arithmetic.cexp (infixr \<open>^c\<close> 90)
alias cinfinite = BNF_Cardinal_Arithmetic.cinfinite
alias czero = BNF_Cardinal_Arithmetic.czero
@@ -69,18 +69,18 @@
begin
notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900)
+ bot (\<open>\<bottom>\<close>) and
+ top (\<open>\<top>\<close>) and
+ inf (infixl \<open>\<sqinter>\<close> 70) and
+ sup (infixl \<open>\<squnion>\<close> 65) and
+ Inf (\<open>\<Sqinter> _\<close> [900] 900) and
+ Sup (\<open>\<Squnion> _\<close> [900] 900)
syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
end
@@ -88,18 +88,18 @@
begin
no_notation
- bot ("\<bottom>") and
- top ("\<top>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter> _" [900] 900) and
- Sup ("\<Squnion> _" [900] 900)
+ bot (\<open>\<bottom>\<close>) and
+ top (\<open>\<top>\<close>) and
+ inf (infixl \<open>\<sqinter>\<close> 70) and
+ sup (infixl \<open>\<squnion>\<close> 65) and
+ Inf (\<open>\<Sqinter> _\<close> [900] 900) and
+ Sup (\<open>\<Squnion> _\<close> [900] 900)
no_syntax
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_./ _)\<close> [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_./ _)\<close> [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
end
--- a/src/HOL/Map.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Map.thy Mon Sep 23 13:32:38 2024 +0200
@@ -12,26 +12,26 @@
abbrevs "(=" = "\<subseteq>\<^sub>m"
begin
-type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
+type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr \<open>\<rightharpoonup>\<close> 0)
abbreviation (input)
empty :: "'a \<rightharpoonup> 'b" where
"empty \<equiv> \<lambda>x. None"
definition
- map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl "\<circ>\<^sub>m" 55) where
+ map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl \<open>\<circ>\<^sub>m\<close> 55) where
"f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
definition
- map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "++" 100) where
+ map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl \<open>++\<close> 100) where
"m1 ++ m2 = (\<lambda>x. case m2 x of None \<Rightarrow> m1 x | Some y \<Rightarrow> Some y)"
definition
- restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "|`" 110) where
+ restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl \<open>|`\<close> 110) where
"m|`A = (\<lambda>x. if x \<in> A then m x else None)"
notation (latex output)
- restrict_map ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
+ restrict_map (\<open>_\<restriction>\<^bsub>_\<^esub>\<close> [111,110] 110)
definition
dom :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a set" where
@@ -46,7 +46,7 @@
"graph m = {(a, b) | a b. m a = Some b}"
definition
- map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<subseteq>\<^sub>m" 50) where
+ map_le :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix \<open>\<subseteq>\<^sub>m\<close> 50) where
"(m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2) \<longleftrightarrow> (\<forall>a \<in> dom m\<^sub>1. m\<^sub>1 a = m\<^sub>2 a)"
text \<open>Function update syntax \<open>f(x := y, \<dots>)\<close> is extended with \<open>x \<mapsto> y\<close>, which is short for
@@ -57,15 +57,15 @@
nonterminal maplet and maplets
syntax
- "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /\<mapsto>/ _")
- "" :: "maplet \<Rightarrow> updbind" ("_")
- "" :: "maplet \<Rightarrow> maplets" ("_")
- "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
- "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" ("(1[_])")
+ "_maplet" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /\<mapsto>/ _\<close>)
+ "" :: "maplet \<Rightarrow> updbind" (\<open>_\<close>)
+ "" :: "maplet \<Rightarrow> maplets" (\<open>_\<close>)
+ "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" (\<open>_,/ _\<close>)
+ "_Map" :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b" (\<open>(1[_])\<close>)
(* Syntax forbids \<open>[\<dots>, x := y, \<dots>]\<close> by introducing \<open>maplets\<close> in addition to \<open>updbinds\<close> *)
syntax (ASCII)
- "_maplet" :: "['a, 'a] \<Rightarrow> maplet" ("_ /|->/ _")
+ "_maplet" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /|->/ _\<close>)
syntax_consts
"_maplet" "_Maplets" "_Map" \<rightleftharpoons> fun_upd
@@ -97,10 +97,10 @@
text \<open>There is also the more specialized update syntax \<open>xs [\<mapsto>] ys\<close> for lists \<open>xs\<close> and \<open>ys\<close>.\<close>
syntax
- "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[\<mapsto>]/ _")
+ "_maplets" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /[\<mapsto>]/ _\<close>)
syntax (ASCII)
- "_maplets" :: "['a, 'a] \<Rightarrow> maplet" ("_ /[|->]/ _")
+ "_maplets" :: "['a, 'a] \<Rightarrow> maplet" (\<open>_ /[|->]/ _\<close>)
syntax_consts
"_maplets" \<rightleftharpoons> map_upds
--- a/src/HOL/Modules.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Modules.thy Mon Sep 23 13:32:38 2024 +0200
@@ -47,7 +47,7 @@
text \<open>Modules form the central spaces in linear algebra. They are a generalization from vector
spaces by replacing the scalar field by a scalar ring.\<close>
locale module =
- fixes scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
+ fixes scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*s\<close> 75)
assumes scale_right_distrib [algebra_simps, algebra_split_simps]:
"a *s (x + y) = a *s x + a *s y"
and scale_left_distrib [algebra_simps, algebra_split_simps]:
@@ -718,8 +718,8 @@
text \<open>A linear function is a mapping between two modules over the same ring.\<close>
locale module_hom = m1: module s1 + m2: module s2
- for s1 :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
- and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75) +
+ for s1 :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*a\<close> 75)
+ and s2 :: "'a::comm_ring_1 \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr \<open>*b\<close> 75) +
fixes f :: "'b \<Rightarrow> 'c"
assumes add: "f (b1 + b2) = f b1 + f b2"
and scale: "f (r *a b) = r *b f b"
--- a/src/HOL/Nat.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Nat.thy Mon Sep 23 13:32:38 2024 +0200
@@ -1463,11 +1463,11 @@
consts compow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
-abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^^" 80)
+abbreviation compower :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr \<open>^^\<close> 80)
where "f ^^ n \<equiv> compow n f"
notation (latex output)
- compower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+ compower (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)
text \<open>\<open>f ^^ n = f \<circ> \<dots> \<circ> f\<close>, the \<open>n\<close>-fold composition of \<open>f\<close>\<close>
@@ -1891,7 +1891,7 @@
context semiring_1
begin
-definition Nats :: "'a set" ("\<nat>")
+definition Nats :: "'a set" (\<open>\<nat>\<close>)
where "\<nat> = range of_nat"
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
--- a/src/HOL/Num.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Num.thy Mon Sep 23 13:32:38 2024 +0200
@@ -302,7 +302,7 @@
text \<open>Numeral syntax.\<close>
syntax
- "_Numeral" :: "num_const \<Rightarrow> 'a" ("_")
+ "_Numeral" :: "num_const \<Rightarrow> 'a" (\<open>_\<close>)
ML_file \<open>Tools/numeral.ML\<close>
--- a/src/HOL/Orderings.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Orderings.thy Mon Sep 23 13:32:38 2024 +0200
@@ -178,25 +178,25 @@
begin
notation
- less_eq ("'(\<le>')") and
- less_eq ("(_/ \<le> _)" [51, 51] 50) and
- less ("'(<')") and
- less ("(_/ < _)" [51, 51] 50)
+ less_eq (\<open>'(\<le>')\<close>) and
+ less_eq (\<open>(_/ \<le> _)\<close> [51, 51] 50) and
+ less (\<open>'(<')\<close>) and
+ less (\<open>(_/ < _)\<close> [51, 51] 50)
abbreviation (input)
- greater_eq (infix "\<ge>" 50)
+ greater_eq (infix \<open>\<ge>\<close> 50)
where "x \<ge> y \<equiv> y \<le> x"
abbreviation (input)
- greater (infix ">" 50)
+ greater (infix \<open>>\<close> 50)
where "x > y \<equiv> y < x"
notation (ASCII)
- less_eq ("'(<=')") and
- less_eq ("(_/ <= _)" [51, 51] 50)
+ less_eq (\<open>'(<=')\<close>) and
+ less_eq (\<open>(_/ <= _)\<close> [51, 51] 50)
notation (input)
- greater_eq (infix ">=" 50)
+ greater_eq (infix \<open>>=\<close> 50)
end
@@ -357,7 +357,7 @@
text \<open>Least value operator\<close>
definition (in ord)
- Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
+ Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder \<open>LEAST \<close> 10) where
"Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
lemma Least_equality:
@@ -384,7 +384,7 @@
text \<open>Greatest value operator\<close>
-definition Greatest :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "GREATEST " 10) where
+definition Greatest :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder \<open>GREATEST \<close> 10) where
"Greatest P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<ge> y))"
lemma GreatestI2_order:
@@ -403,8 +403,8 @@
end
lemma ordering_orderI:
- fixes less_eq (infix "\<^bold>\<le>" 50)
- and less (infix "\<^bold><" 50)
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
assumes "ordering less_eq less"
shows "class.order less_eq less"
proof -
@@ -414,8 +414,8 @@
qed
lemma order_strictI:
- fixes less (infix "\<^bold><" 50)
- and less_eq (infix "\<^bold>\<le>" 50)
+ fixes less (infix \<open>\<^bold><\<close> 50)
+ and less_eq (infix \<open>\<^bold>\<le>\<close> 50)
assumes "\<And>a b. a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>< b \<or> a = b"
assumes "\<And>a b. a \<^bold>< b \<Longrightarrow> \<not> b \<^bold>< a"
assumes "\<And>a. \<not> a \<^bold>< a"
@@ -506,8 +506,8 @@
text \<open>Alternative introduction rule with bias towards strict order\<close>
lemma linorder_strictI:
- fixes less_eq (infix "\<^bold>\<le>" 50)
- and less (infix "\<^bold><" 50)
+ fixes less_eq (infix \<open>\<^bold>\<le>\<close> 50)
+ and less (infix \<open>\<^bold><\<close> 50)
assumes "class.order less_eq less"
assumes trichotomy: "\<And>a b. a \<^bold>< b \<or> a = b \<or> b \<^bold>< a"
shows "class.linorder less_eq less"
@@ -710,40 +710,40 @@
subsection \<open>Bounded quantifiers\<close>
syntax (ASCII)
- "_All_less" :: "[idt, 'a, bool] => bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3EX _<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
- "_All_greater" :: "[idt, 'a, bool] => bool" ("(3ALL _>_./ _)" [0, 0, 10] 10)
- "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3EX _>_./ _)" [0, 0, 10] 10)
- "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3ALL _>=_./ _)" [0, 0, 10] 10)
- "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3EX _>=_./ _)" [0, 0, 10] 10)
+ "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(3EX _>_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _>=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _>=_./ _)\<close> [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" ("(3ALL _~=_./ _)" [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3EX _~=_./ _)" [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3ALL _~=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3EX _~=_./ _)\<close> [0, 0, 10] 10)
syntax
- "_All_less" :: "[idt, 'a, bool] => bool" ("(3\<forall>_<_./ _)" [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3\<exists>_<_./ _)" [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<le>_./ _)" [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<le>_./ _)\<close> [0, 0, 10] 10)
- "_All_greater" :: "[idt, 'a, bool] => bool" ("(3\<forall>_>_./ _)" [0, 0, 10] 10)
- "_Ex_greater" :: "[idt, 'a, bool] => bool" ("(3\<exists>_>_./ _)" [0, 0, 10] 10)
- "_All_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<ge>_./ _)" [0, 0, 10] 10)
- "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<ge>_./ _)" [0, 0, 10] 10)
+ "_All_greater" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_>_./ _)\<close> [0, 0, 10] 10)
+ "_All_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<ge>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_greater_eq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<ge>_./ _)\<close> [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" ("(3\<forall>_\<noteq>_./ _)" [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3\<exists>_\<noteq>_./ _)" [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3\<forall>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3\<exists>_\<noteq>_./ _)\<close> [0, 0, 10] 10)
syntax (input)
- "_All_less" :: "[idt, 'a, bool] => bool" ("(3! _<_./ _)" [0, 0, 10] 10)
- "_Ex_less" :: "[idt, 'a, bool] => bool" ("(3? _<_./ _)" [0, 0, 10] 10)
- "_All_less_eq" :: "[idt, 'a, bool] => bool" ("(3! _<=_./ _)" [0, 0, 10] 10)
- "_Ex_less_eq" :: "[idt, 'a, bool] => bool" ("(3? _<=_./ _)" [0, 0, 10] 10)
- "_All_neq" :: "[idt, 'a, bool] => bool" ("(3! _~=_./ _)" [0, 0, 10] 10)
- "_Ex_neq" :: "[idt, 'a, bool] => bool" ("(3? _~=_./ _)" [0, 0, 10] 10)
+ "_All_less" :: "[idt, 'a, bool] => bool" (\<open>(3! _<_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less" :: "[idt, 'a, bool] => bool" (\<open>(3? _<_./ _)\<close> [0, 0, 10] 10)
+ "_All_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3! _<=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_less_eq" :: "[idt, 'a, bool] => bool" (\<open>(3? _<=_./ _)\<close> [0, 0, 10] 10)
+ "_All_neq" :: "[idt, 'a, bool] => bool" (\<open>(3! _~=_./ _)\<close> [0, 0, 10] 10)
+ "_Ex_neq" :: "[idt, 'a, bool] => bool" (\<open>(3? _~=_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_All_less" "_All_less_eq" "_All_greater" "_All_greater_eq" "_All_neq" \<rightleftharpoons> All and
@@ -1141,7 +1141,7 @@
subsection \<open>(Unique) top and bottom elements\<close>
class bot =
- fixes bot :: 'a ("\<bottom>")
+ fixes bot :: 'a (\<open>\<bottom>\<close>)
class order_bot = order + bot +
assumes bot_least: "\<bottom> \<le> a"
@@ -1181,7 +1181,7 @@
end
class top =
- fixes top :: 'a ("\<top>")
+ fixes top :: 'a (\<open>\<top>\<close>)
class order_top = order + top +
assumes top_greatest: "a \<le> \<top>"
--- a/src/HOL/Power.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Power.thy Mon Sep 23 13:32:38 2024 +0200
@@ -14,16 +14,16 @@
class power = one + times
begin
-primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
+primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr \<open>^\<close> 80)
where
power_0: "a ^ 0 = 1"
| power_Suc: "a ^ Suc n = a * a ^ n"
notation (latex output)
- power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+ power (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)
text \<open>Special syntax for squares.\<close>
-abbreviation power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999)
+abbreviation power2 :: "'a \<Rightarrow> 'a" (\<open>(_\<^sup>2)\<close> [1000] 999)
where "x\<^sup>2 \<equiv> x ^ 2"
end
--- a/src/HOL/Predicate.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Predicate.thy Mon Sep 23 13:32:38 2024 +0200
@@ -126,7 +126,7 @@
"eval (single x) = (=) x"
by (simp add: single_def)
-definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl "\<bind>" 70) where
+definition bind :: "'a pred \<Rightarrow> ('a \<Rightarrow> 'b pred) \<Rightarrow> 'b pred" (infixl \<open>\<bind>\<close> 70) where
"P \<bind> f = (\<Squnion>(f ` {x. eval P x}))"
lemma eval_bind [simp]:
@@ -728,7 +728,7 @@
by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
no_notation
- bind (infixl "\<bind>" 70)
+ bind (infixl \<open>\<bind>\<close> 70)
hide_type (open) pred seq
hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
--- a/src/HOL/Product_Type.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Product_Type.thy Mon Sep 23 13:32:38 2024 +0200
@@ -61,7 +61,7 @@
typedef unit = "{True}"
by auto
-definition Unity :: unit ("'(')")
+definition Unity :: unit (\<open>'(')\<close>)
where "() = Abs_unit True"
lemma unit_eq [no_atp]: "u = ()"
@@ -214,11 +214,11 @@
definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
-typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (\<open>(_ \<times>/ _)\<close> [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
unfolding prod_def by auto
type_notation (ASCII)
- prod (infixr "*" 20)
+ prod (infixr \<open>*\<close> 20)
definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b"
where "Pair a b = Abs_prod (Pair_Rep a b)"
@@ -286,13 +286,13 @@
nonterminal tuple_args and patterns
syntax
- "_tuple" :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b" ("(1'(_,/ _'))")
- "_tuple_arg" :: "'a \<Rightarrow> tuple_args" ("_")
- "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args" ("_,/ _")
- "_pattern" :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn" ("'(_,/ _')")
- "" :: "pttrn \<Rightarrow> patterns" ("_")
- "_patterns" :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns" ("_,/ _")
- "_unit" :: pttrn ("'(')")
+ "_tuple" :: "'a \<Rightarrow> tuple_args \<Rightarrow> 'a \<times> 'b" (\<open>(1'(_,/ _'))\<close>)
+ "_tuple_arg" :: "'a \<Rightarrow> tuple_args" (\<open>_\<close>)
+ "_tuple_args" :: "'a \<Rightarrow> tuple_args \<Rightarrow> tuple_args" (\<open>_,/ _\<close>)
+ "_pattern" :: "pttrn \<Rightarrow> patterns \<Rightarrow> pttrn" (\<open>'(_,/ _')\<close>)
+ "" :: "pttrn \<Rightarrow> patterns" (\<open>_\<close>)
+ "_patterns" :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns" (\<open>_,/ _\<close>)
+ "_unit" :: pttrn (\<open>'(')\<close>)
syntax_consts
"_tuple" "_tuple_arg" "_tuple_args" \<rightleftharpoons> Pair and
"_pattern" "_patterns" \<rightleftharpoons> case_prod and
@@ -797,16 +797,16 @@
text \<open>The composition-uncurry combinator.\<close>
-definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl "\<circ>\<rightarrow>" 60)
+definition scomp :: "('a \<Rightarrow> 'b \<times> 'c) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> 'a \<Rightarrow> 'd" (infixl \<open>\<circ>\<rightarrow>\<close> 60)
where "f \<circ>\<rightarrow> g = (\<lambda>x. case_prod g (f x))"
-no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
+no_notation scomp (infixl \<open>\<circ>\<rightarrow>\<close> 60)
bundle state_combinator_syntax
begin
-notation fcomp (infixl "\<circ>>" 60)
-notation scomp (infixl "\<circ>\<rightarrow>" 60)
+notation fcomp (infixl \<open>\<circ>>\<close> 60)
+notation scomp (infixl \<open>\<circ>\<rightarrow>\<close> 60)
end
@@ -1000,20 +1000,20 @@
definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
-abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr "\<times>" 80)
+abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr \<open>\<times>\<close> 80)
where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
hide_const (open) Times
bundle no_Set_Product_syntax begin
-no_notation Product_Type.Times (infixr "\<times>" 80)
+no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
bundle Set_Product_syntax begin
-notation Product_Type.Times (infixr "\<times>" 80)
+notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
syntax
- "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" ("(3SIGMA _:_./ _)" [0, 0, 10] 10)
+ "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (\<open>(3SIGMA _:_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_Sigma" \<rightleftharpoons> Sigma
translations
--- a/src/HOL/Quickcheck_Exhaustive.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy Mon Sep 23 13:32:38 2024 +0200
@@ -11,7 +11,7 @@
subsection \<open>Basic operations for exhaustive generators\<close>
-definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" (infixr "orelse" 55)
+definition orelse :: "'a option \<Rightarrow> 'a option \<Rightarrow> 'a option" (infixr \<open>orelse\<close> 55)
where [code_unfold]: "x orelse y = (case x of Some x' \<Rightarrow> Some x' | None \<Rightarrow> y)"
@@ -738,7 +738,7 @@
axiomatization unknown :: 'a
-notation (output) unknown ("?")
+notation (output) unknown (\<open>?\<close>)
ML_file \<open>Tools/Quickcheck/exhaustive_generators.ML\<close>
@@ -750,7 +750,7 @@
ML_file \<open>Tools/Quickcheck/abstract_generators.ML\<close>
hide_fact (open) orelse_def
-no_notation orelse (infixr "orelse" 55)
+no_notation orelse (infixr \<open>orelse\<close> 55)
hide_const valtermify_absdummy valtermify_fun_upd
valterm_emptyset valtermify_insert
--- a/src/HOL/Quotient.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Quotient.thy Mon Sep 23 13:32:38 2024 +0200
@@ -22,7 +22,7 @@
text \<open>Composition of Relations\<close>
abbreviation
- rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
+ rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr \<open>OOO\<close> 75)
where
"r1 OOO r2 \<equiv> r1 OO r2 OO r1"
@@ -746,7 +746,7 @@
\<open>lift theorems to quotient types\<close>
no_notation
- rel_conj (infixr "OOO" 75)
+ rel_conj (infixr \<open>OOO\<close> 75)
section \<open>Lifting of BNFs\<close>
--- a/src/HOL/Rat.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Rat.thy Mon Sep 23 13:32:38 2024 +0200
@@ -800,7 +800,7 @@
context field_char_0
begin
-definition Rats :: "'a set" ("\<rat>")
+definition Rats :: "'a set" (\<open>\<rat>\<close>)
where "\<rat> = range of_rat"
end
@@ -1155,7 +1155,7 @@
subsection \<open>Float syntax\<close>
-syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_")
+syntax "_Float" :: "float_const \<Rightarrow> 'a" (\<open>_\<close>)
parse_translation \<open>
let
--- a/src/HOL/Real_Vector_Spaces.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Sep 23 13:32:38 2024 +0200
@@ -12,10 +12,10 @@
subsection \<open>Real vector spaces\<close>
class scaleR =
- fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
+ fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr \<open>*\<^sub>R\<close> 75)
begin
-abbreviation divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl "'/\<^sub>R" 70)
+abbreviation divideR :: "'a \<Rightarrow> real \<Rightarrow> 'a" (infixl \<open>'/\<^sub>R\<close> 70)
where "x /\<^sub>R r \<equiv> inverse r *\<^sub>R x"
end
@@ -409,7 +409,7 @@
subsection \<open>The Set of Real Numbers\<close>
-definition Reals :: "'a::real_algebra_1 set" ("\<real>")
+definition Reals :: "'a::real_algebra_1 set" (\<open>\<real>\<close>)
where "\<real> = range of_real"
lemma Reals_of_real [simp]: "of_real r \<in> \<real>"
@@ -1535,7 +1535,7 @@
locale bounded_bilinear =
fixes prod :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
- (infixl "**" 70)
+ (infixl \<open>**\<close> 70)
assumes add_left: "prod (a + a') b = prod a b + prod a' b"
and add_right: "prod a (b + b') = prod a b + prod a b'"
and scaleR_left: "prod (scaleR r a) b = scaleR r (prod a b)"
--- a/src/HOL/Record.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Record.thy Mon Sep 23 13:32:38 2024 +0200
@@ -423,32 +423,32 @@
field_updates
syntax
- "_constify" :: "id => ident" ("_")
- "_constify" :: "longid => ident" ("_")
+ "_constify" :: "id => ident" (\<open>_\<close>)
+ "_constify" :: "longid => ident" (\<open>_\<close>)
- "_field_type" :: "ident => type => field_type" ("(2_ ::/ _)")
- "" :: "field_type => field_types" ("_")
- "_field_types" :: "field_type => field_types => field_types" ("_,/ _")
- "_record_type" :: "field_types => type" ("(3\<lparr>_\<rparr>)")
- "_record_type_scheme" :: "field_types => type => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
+ "_field_type" :: "ident => type => field_type" (\<open>(2_ ::/ _)\<close>)
+ "" :: "field_type => field_types" (\<open>_\<close>)
+ "_field_types" :: "field_type => field_types => field_types" (\<open>_,/ _\<close>)
+ "_record_type" :: "field_types => type" (\<open>(3\<lparr>_\<rparr>)\<close>)
+ "_record_type_scheme" :: "field_types => type => type" (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
- "_field" :: "ident => 'a => field" ("(2_ =/ _)")
- "" :: "field => fields" ("_")
- "_fields" :: "field => fields => fields" ("_,/ _")
- "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)")
- "_record_scheme" :: "fields => 'a => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
+ "_field" :: "ident => 'a => field" (\<open>(2_ =/ _)\<close>)
+ "" :: "field => fields" (\<open>_\<close>)
+ "_fields" :: "field => fields => fields" (\<open>_,/ _\<close>)
+ "_record" :: "fields => 'a" (\<open>(3\<lparr>_\<rparr>)\<close>)
+ "_record_scheme" :: "fields => 'a => 'a" (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
- "_field_update" :: "ident => 'a => field_update" ("(2_ :=/ _)")
- "" :: "field_update => field_updates" ("_")
- "_field_updates" :: "field_update => field_updates => field_updates" ("_,/ _")
- "_record_update" :: "'a => field_updates => 'b" ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+ "_field_update" :: "ident => 'a => field_update" (\<open>(2_ :=/ _)\<close>)
+ "" :: "field_update => field_updates" (\<open>_\<close>)
+ "_field_updates" :: "field_update => field_updates => field_updates" (\<open>_,/ _\<close>)
+ "_record_update" :: "'a => field_updates => 'b" (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
syntax (ASCII)
- "_record_type" :: "field_types => type" ("(3'(| _ |'))")
- "_record_type_scheme" :: "field_types => type => type" ("(3'(| _,/ (2... ::/ _) |'))")
- "_record" :: "fields => 'a" ("(3'(| _ |'))")
- "_record_scheme" :: "fields => 'a => 'a" ("(3'(| _,/ (2... =/ _) |'))")
- "_record_update" :: "'a => field_updates => 'b" ("_/(3'(| _ |'))" [900, 0] 900)
+ "_record_type" :: "field_types => type" (\<open>(3'(| _ |'))\<close>)
+ "_record_type_scheme" :: "field_types => type => type" (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
+ "_record" :: "fields => 'a" (\<open>(3'(| _ |'))\<close>)
+ "_record_scheme" :: "fields => 'a => 'a" (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
+ "_record_update" :: "'a => field_updates => 'b" (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
subsection \<open>Record package\<close>
--- a/src/HOL/Relation.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Relation.thy Mon Sep 23 13:32:38 2024 +0200
@@ -969,11 +969,11 @@
subsubsection \<open>Composition\<close>
-inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr "O" 75)
+inductive_set relcomp :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'c) set \<Rightarrow> ('a \<times> 'c) set" (infixr \<open>O\<close> 75)
for r :: "('a \<times> 'b) set" and s :: "('b \<times> 'c) set"
where relcompI [intro]: "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> s \<Longrightarrow> (a, c) \<in> r O s"
-notation relcompp (infixr "OO" 75)
+notation relcompp (infixr \<open>OO\<close> 75)
lemmas relcomppI = relcompp.intros
@@ -1074,15 +1074,15 @@
subsubsection \<open>Converse\<close>
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_\<inverse>)" [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" (\<open>(_\<inverse>)\<close> [1000] 999)
for r :: "('a \<times> 'b) set"
where "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
-notation conversep ("(_\<inverse>\<inverse>)" [1000] 1000)
+notation conversep (\<open>(_\<inverse>\<inverse>)\<close> [1000] 1000)
notation (ASCII)
- converse ("(_^-1)" [1000] 999) and
- conversep ("(_^--1)" [1000] 1000)
+ converse (\<open>(_^-1)\<close> [1000] 999) and
+ conversep (\<open>(_^--1)\<close> [1000] 1000)
lemma converseI [sym]: "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
by (fact converse.intros)
@@ -1386,7 +1386,7 @@
subsubsection \<open>Image of a set under a relation\<close>
-definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "``" 90)
+definition Image :: "('a \<times> 'b) set \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr \<open>``\<close> 90)
where "r `` s = {y. \<exists>x\<in>s. (x, y) \<in> r}"
lemma Image_iff: "b \<in> r``A \<longleftrightarrow> (\<exists>x\<in>A. (x, b) \<in> r)"
--- a/src/HOL/Rings.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Rings.thy Mon Sep 23 13:32:38 2024 +0200
@@ -147,7 +147,7 @@
class dvd = times
begin
-definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "dvd" 50)
+definition dvd :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>dvd\<close> 50)
where "b dvd a \<longleftrightarrow> (\<exists>k. a = b * k)"
lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
@@ -680,7 +680,7 @@
subsection \<open>(Partial) Division\<close>
class divide =
- fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
+ fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>div\<close> 70)
setup \<open>Sign.add_const_constraint (\<^const_name>\<open>divide\<close>, SOME \<^typ>\<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>)\<close>
@@ -1722,7 +1722,7 @@
text \<open>Syntactic division remainder operator\<close>
class modulo = dvd + divide +
- fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
+ fixes modulo :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl \<open>mod\<close> 70)
text \<open>Arbitrary quotient and remainder partitions\<close>
--- a/src/HOL/Series.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Series.thy Mon Sep 23 13:32:38 2024 +0200
@@ -16,14 +16,14 @@
subsection \<open>Definition of infinite summability\<close>
definition sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
- (infixr "sums" 80)
+ (infixr \<open>sums\<close> 80)
where "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s"
definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool"
where "summable f \<longleftrightarrow> (\<exists>s. f sums s)"
definition suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a"
- (binder "\<Sum>" 10)
+ (binder \<open>\<Sum>\<close> 10)
where "suminf f = (THE s. f sums s)"
text\<open>Variants of the definition\<close>
--- a/src/HOL/Set.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Set.thy Mon Sep 23 13:32:38 2024 +0200
@@ -20,35 +20,35 @@
and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
notation
- member ("'(\<in>')") and
- member ("(_/ \<in> _)" [51, 51] 50)
+ member (\<open>'(\<in>')\<close>) and
+ member (\<open>(_/ \<in> _)\<close> [51, 51] 50)
abbreviation not_member
where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> \<open>non-membership\<close>
notation
- not_member ("'(\<notin>')") and
- not_member ("(_/ \<notin> _)" [51, 51] 50)
+ not_member (\<open>'(\<notin>')\<close>) and
+ not_member (\<open>(_/ \<notin> _)\<close> [51, 51] 50)
notation (ASCII)
- member ("'(:')") and
- member ("(_/ : _)" [51, 51] 50) and
- not_member ("'(~:')") and
- not_member ("(_/ ~: _)" [51, 51] 50)
+ member (\<open>'(:')\<close>) and
+ member (\<open>(_/ : _)\<close> [51, 51] 50) and
+ not_member (\<open>'(~:')\<close>) and
+ not_member (\<open>(_/ ~: _)\<close> [51, 51] 50)
text \<open>Set comprehensions\<close>
syntax
- "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_./ _})")
+ "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{_./ _})\<close>)
syntax_consts
"_Coll" \<rightleftharpoons> Collect
translations
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
syntax (ASCII)
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/: _)./ _})")
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{(_/: _)./ _})\<close>)
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{(_/ \<in> _)./ _})")
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{(_/ \<in> _)./ _})\<close>)
syntax_consts
"_Collect" \<rightleftharpoons> Collect
translations
@@ -137,7 +137,7 @@
text \<open>Set enumerations\<close>
-abbreviation empty :: "'a set" ("{}")
+abbreviation empty :: "'a set" (\<open>{}\<close>)
where "{} \<equiv> bot"
definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
@@ -145,9 +145,9 @@
nonterminal finset_args
syntax
- "" :: "'a \<Rightarrow> finset_args" ("_")
- "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args" ("_,/ _")
- "_Finset" :: "finset_args \<Rightarrow> 'a set" ("{(_)}")
+ "" :: "'a \<Rightarrow> finset_args" (\<open>_\<close>)
+ "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args" (\<open>_,/ _\<close>)
+ "_Finset" :: "finset_args \<Rightarrow> 'a set" (\<open>{(_)}\<close>)
syntax_consts
"_Finset_args" "_Finset" \<rightleftharpoons> insert
translations
@@ -164,10 +164,10 @@
where "subset_eq \<equiv> less_eq"
notation
- subset ("'(\<subset>')") and
- subset ("(_/ \<subset> _)" [51, 51] 50) and
- subset_eq ("'(\<subseteq>')") and
- subset_eq ("(_/ \<subseteq> _)" [51, 51] 50)
+ subset (\<open>'(\<subset>')\<close>) and
+ subset (\<open>(_/ \<subset> _)\<close> [51, 51] 50) and
+ subset_eq (\<open>'(\<subseteq>')\<close>) and
+ subset_eq (\<open>(_/ \<subseteq> _)\<close> [51, 51] 50)
abbreviation (input)
supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -178,16 +178,16 @@
"supset_eq \<equiv> greater_eq"
notation
- supset ("'(\<supset>')") and
- supset ("(_/ \<supset> _)" [51, 51] 50) and
- supset_eq ("'(\<supseteq>')") and
- supset_eq ("(_/ \<supseteq> _)" [51, 51] 50)
+ supset (\<open>'(\<supset>')\<close>) and
+ supset (\<open>(_/ \<supset> _)\<close> [51, 51] 50) and
+ supset_eq (\<open>'(\<supseteq>')\<close>) and
+ supset_eq (\<open>(_/ \<supseteq> _)\<close> [51, 51] 50)
notation (ASCII output)
- subset ("'(<')") and
- subset ("(_/ < _)" [51, 51] 50) and
- subset_eq ("'(<=')") and
- subset_eq ("(_/ <= _)" [51, 51] 50)
+ subset (\<open>'(<')\<close>) and
+ subset (\<open>(_/ < _)\<close> [51, 51] 50) and
+ subset_eq (\<open>'(<=')\<close>) and
+ subset_eq (\<open>(_/ <= _)\<close> [51, 51] 50)
definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
where "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)" \<comment> \<open>bounded universal quantifiers\<close>
@@ -196,21 +196,21 @@
where "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)" \<comment> \<open>bounded existential quantifiers\<close>
syntax (ASCII)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3ALL (_/:_)./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX (_/:_)./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3EX! (_/:_)./ _)" [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST (_/:_)./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3ALL (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3EX! (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3LEAST (_/:_)./ _)\<close> [0, 0, 10] 10)
syntax (input)
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3! (_/:_)./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3? (_/:_)./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3?! (_/:_)./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3! (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3? (_/:_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3?! (_/:_)./ _)\<close> [0, 0, 10] 10)
syntax
- "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>(_/\<in>_)./ _)" [0, 0, 10] 10)
- "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>(_/\<in>_)./ _)" [0, 0, 10] 10)
- "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
- "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
+ "_Ball" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bex1" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>!(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
+ "_Bleast" :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a" (\<open>(3LEAST(_/\<in>_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_Ball" \<rightleftharpoons> Ball and
@@ -225,18 +225,18 @@
"LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
syntax (ASCII output)
- "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3ALL _<_./ _)" [0, 0, 10] 10)
- "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3EX _<_./ _)" [0, 0, 10] 10)
- "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3ALL _<=_./ _)" [0, 0, 10] 10)
- "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3EX _<=_./ _)" [0, 0, 10] 10)
- "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3EX! _<=_./ _)" [0, 0, 10] 10)
+ "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3ALL _<_./ _)\<close> [0, 0, 10] 10)
+ "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX _<_./ _)\<close> [0, 0, 10] 10)
+ "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3ALL _<=_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX _<=_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3EX! _<=_./ _)\<close> [0, 0, 10] 10)
syntax
- "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<forall>_\<subset>_./ _)" [0, 0, 10] 10)
- "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<exists>_\<subset>_./ _)" [0, 0, 10] 10)
- "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
- "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
- "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
+ "_setlessAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<forall>_\<subset>_./ _)\<close> [0, 0, 10] 10)
+ "_setlessEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>_\<subset>_./ _)\<close> [0, 0, 10] 10)
+ "_setleAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<forall>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
+ "_setleEx1" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(3\<exists>!_\<subseteq>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_setlessAll" "_setleAll" \<rightleftharpoons> All and
@@ -291,7 +291,7 @@
\<close>
syntax
- "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set" ("(1{_ |/_./ _})")
+ "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(1{_ |/_./ _})\<close>)
syntax_consts
"_Setcompr" \<rightleftharpoons> Collect
@@ -662,11 +662,11 @@
subsubsection \<open>Binary intersection\<close>
-abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<inter>" 70)
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl \<open>\<inter>\<close> 70)
where "(\<inter>) \<equiv> inf"
notation (ASCII)
- inter (infixl "Int" 70)
+ inter (infixl \<open>Int\<close> 70)
lemma Int_def: "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
by (simp add: inf_set_def inf_fun_def)
@@ -689,11 +689,11 @@
subsubsection \<open>Binary union\<close>
-abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "\<union>" 65)
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl \<open>\<union>\<close> 65)
where "union \<equiv> sup"
notation (ASCII)
- union (infixl "Un" 65)
+ union (infixl \<open>Un\<close> 65)
lemma Un_def: "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
by (simp add: sup_set_def sup_fun_def)
@@ -861,7 +861,7 @@
text \<open>Frequently \<open>b\<close> does not have the syntactic form of \<open>f x\<close>.\<close>
-definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr "`" 90)
+definition image :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set" (infixr \<open>`\<close> 90)
where "f ` A = {y. \<exists>x\<in>A. y = f x}"
lemma image_eqI [simp, intro]: "b = f x \<Longrightarrow> x \<in> A \<Longrightarrow> b \<in> f ` A"
@@ -1712,7 +1712,7 @@
subsubsection \<open>Inverse image of a function\<close>
-definition vimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a set" (infixr "-`" 90)
+definition vimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a set" (infixr \<open>-`\<close> 90)
where "f -` B \<equiv> {x. f x \<in> B}"
lemma vimage_eq [simp]: "a \<in> f -` B \<longleftrightarrow> f a \<in> B"
--- a/src/HOL/Set_Interval.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Set_Interval.thy Mon Sep 23 13:32:38 2024 +0200
@@ -29,35 +29,35 @@
begin
definition
- lessThan :: "'a => 'a set" ("(1{..<_})") where
+ lessThan :: "'a => 'a set" (\<open>(1{..<_})\<close>) where
"{..<u} == {x. x < u}"
definition
- atMost :: "'a => 'a set" ("(1{.._})") where
+ atMost :: "'a => 'a set" (\<open>(1{.._})\<close>) where
"{..u} == {x. x \<le> u}"
definition
- greaterThan :: "'a => 'a set" ("(1{_<..})") where
+ greaterThan :: "'a => 'a set" (\<open>(1{_<..})\<close>) where
"{l<..} == {x. l<x}"
definition
- atLeast :: "'a => 'a set" ("(1{_..})") where
+ atLeast :: "'a => 'a set" (\<open>(1{_..})\<close>) where
"{l..} == {x. l\<le>x}"
definition
- greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where
+ greaterThanLessThan :: "'a => 'a => 'a set" (\<open>(1{_<..<_})\<close>) where
"{l<..<u} == {l<..} Int {..<u}"
definition
- atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where
+ atLeastLessThan :: "'a => 'a => 'a set" (\<open>(1{_..<_})\<close>) where
"{l..<u} == {l..} Int {..<u}"
definition
- greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where
+ greaterThanAtMost :: "'a => 'a => 'a set" (\<open>(1{_<.._})\<close>) where
"{l<..u} == {l<..} Int {..u}"
definition
- atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where
+ atLeastAtMost :: "'a => 'a => 'a set" (\<open>(1{_.._})\<close>) where
"{l..u} == {l..} Int {..u}"
end
@@ -67,22 +67,22 @@
\<^term>\<open>{m..<n}\<close> may not exist in \<^term>\<open>{..<n}\<close>-form as well.\<close>
syntax (ASCII)
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<=_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3UN _<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<=_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3INT _<_./ _)\<close> [0, 0, 10] 10)
syntax (latex output)
- "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" (\<open>(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)\<close> [0, 0, 10] 10)
syntax
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Union>_<_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_\<le>_./ _)\<close> [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" (\<open>(3\<Inter>_<_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_UNION_le" "_UNION_less" \<rightleftharpoons> Union and
@@ -1988,26 +1988,26 @@
subsection \<open>Summation indexed over intervals\<close>
syntax (ASCII)
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(SUM _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_sum output)
"_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ < _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
"_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\sum_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
- "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
+ "_from_to_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_sum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Sum>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_sum" "_from_upto_sum" "_upt_sum" "_upto_sum" == sum
@@ -2681,26 +2681,26 @@
subsection \<open>Products indexed over intervals\<close>
syntax (ASCII)
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(PROD _<=_./ _)\<close> [0,0,10] 10)
syntax (latex_prod output)
"_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ = _\<^latex>\<open>}^{\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)" [0,0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ = _\<^latex>\<open>}^{<\<close>_\<^latex>\<open>}$\<close> _)\<close> [0,0,0,10] 10)
"_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ < _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
"_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
- ("(3\<^latex>\<open>$\\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)" [0,0,10] 10)
+ (\<open>(3\<^latex>\<open>$\prod_{\<close>_ \<le> _\<^latex>\<open>}$\<close> _)\<close> [0,0,10] 10)
syntax
- "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
- "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
- "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
- "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+ "_from_to_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _.._./ _)\<close> [0,0,0,10] 10)
+ "_from_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_ = _..<_./ _)\<close> [0,0,0,10] 10)
+ "_upt_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_<_./ _)\<close> [0,0,10] 10)
+ "_upto_prod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" (\<open>(3\<Prod>_\<le>_./ _)\<close> [0,0,10] 10)
syntax_consts
"_from_to_prod" "_from_upto_prod" "_upt_prod" "_upto_prod" \<rightleftharpoons> prod
--- a/src/HOL/String.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/String.thy Mon Sep 23 13:32:38 2024 +0200
@@ -216,15 +216,15 @@
by (cases c) simp
syntax
- "_Char" :: "str_position \<Rightarrow> char" ("CHR _")
- "_Char_ord" :: "num_const \<Rightarrow> char" ("CHR _")
+ "_Char" :: "str_position \<Rightarrow> char" (\<open>CHR _\<close>)
+ "_Char_ord" :: "num_const \<Rightarrow> char" (\<open>CHR _\<close>)
syntax_consts
"_Char" "_Char_ord" \<rightleftharpoons> Char
type_synonym string = "char list"
syntax
- "_String" :: "str_position \<Rightarrow> string" ("_")
+ "_String" :: "str_position \<Rightarrow> string" (\<open>_\<close>)
ML_file \<open>Tools/string_syntax.ML\<close>
@@ -522,8 +522,8 @@
code_datatype "0 :: String.literal" String.Literal
syntax
- "_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
- "_Ascii" :: "num_const \<Rightarrow> String.literal" ("STR _")
+ "_Literal" :: "str_position \<Rightarrow> String.literal" (\<open>STR _\<close>)
+ "_Ascii" :: "num_const \<Rightarrow> String.literal" (\<open>STR _\<close>)
syntax_consts
"_Literal" "_Ascii" \<rightleftharpoons> String.Literal
--- a/src/HOL/Sum_Type.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Sum_Type.thy Mon Sep 23 13:32:38 2024 +0200
@@ -19,7 +19,7 @@
definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
-typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
+typedef ('a, 'b) sum (infixr \<open>+\<close> 10) = "sum :: ('a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool) set"
unfolding sum_def by auto
lemma Inl_RepI: "Inl_Rep a \<in> sum"
@@ -209,7 +209,7 @@
subsection \<open>The Disjoint Sum of Sets\<close>
-definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr "<+>" 65)
+definition Plus :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a + 'b) set" (infixr \<open><+>\<close> 65)
where "A <+> B = Inl ` A \<union> Inr ` B"
hide_const (open) Plus \<comment> \<open>Valuable identifier\<close>
--- a/src/HOL/Topological_Spaces.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Sep 23 13:32:38 2024 +0200
@@ -462,10 +462,10 @@
where "nhds a = (INF S\<in>{S. open S \<and> a \<in> S}. principal S)"
definition (in topological_space) at_within :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a filter"
- ("at (_)/ within (_)" [1000, 60] 60)
+ (\<open>at (_)/ within (_)\<close> [1000, 60] 60)
where "at a within s = inf (nhds a) (principal (s - {a}))"
-abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" ("at")
+abbreviation (in topological_space) at :: "'a \<Rightarrow> 'a filter" (\<open>at\<close>)
where "at x \<equiv> at x within (CONST UNIV)"
abbreviation (in order_topology) at_right :: "'a \<Rightarrow> 'a filter"
@@ -746,7 +746,7 @@
subsubsection \<open>Tendsto\<close>
abbreviation (in topological_space)
- tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "\<longlongrightarrow>" 55)
+ tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr \<open>\<longlongrightarrow>\<close> 55)
where "(f \<longlongrightarrow> l) F \<equiv> filterlim f (nhds l) F"
definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -1191,7 +1191,7 @@
subsection \<open>Limits on sequences\<close>
abbreviation (in topological_space)
- LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" ("((_)/ \<longlonglongrightarrow> (_))" [60, 60] 60)
+ LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool" (\<open>((_)/ \<longlonglongrightarrow> (_))\<close> [60, 60] 60)
where "X \<longlonglongrightarrow> L \<equiv> (X \<longlongrightarrow> L) sequentially"
abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -1760,7 +1760,7 @@
subsection \<open>Function limit at a point\<close>
abbreviation LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
- ("((_)/ \<midarrow>(_)/\<rightarrow> (_))" [60, 0, 60] 60)
+ (\<open>((_)/ \<midarrow>(_)/\<rightarrow> (_))\<close> [60, 0, 60] 60)
where "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
--- a/src/HOL/Transcendental.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Transcendental.thy Mon Sep 23 13:32:38 2024 +0200
@@ -1564,7 +1564,7 @@
fixes ln :: "'a \<Rightarrow> 'a"
assumes ln_one [simp]: "ln 1 = 0"
-definition powr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a::ln" (infixr "powr" 80)
+definition powr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a::ln" (infixr \<open>powr\<close> 80)
\<comment> \<open>exponentation via ln and exp\<close>
where "x powr a \<equiv> if x = 0 then 0 else exp (a * ln x)"
--- a/src/HOL/Transfer.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Transfer.thy Mon Sep 23 13:32:38 2024 +0200
@@ -13,8 +13,8 @@
bundle lifting_syntax
begin
- notation rel_fun (infixr "===>" 55)
- notation map_fun (infixr "--->" 55)
+ notation rel_fun (infixr \<open>===>\<close> 55)
+ notation map_fun (infixr \<open>--->\<close> 55)
end
context includes lifting_syntax
--- a/src/HOL/Transitive_Closure.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy Mon Sep 23 13:32:38 2024 +0200
@@ -26,21 +26,21 @@
context notes [[inductive_internals]]
begin
-inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>*)" [1000] 999)
+inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>*)\<close> [1000] 999)
for r :: "('a \<times> 'a) set"
where
rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
-inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>+)" [1000] 999)
+inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>+)\<close> [1000] 999)
for r :: "('a \<times> 'a) set"
where
r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
notation
- rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
- tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000)
+ rtranclp (\<open>(_\<^sup>*\<^sup>*)\<close> [1000] 1000) and
+ tranclp (\<open>(_\<^sup>+\<^sup>+)\<close> [1000] 1000)
declare
rtrancl_def [nitpick_unfold del]
@@ -50,19 +50,19 @@
end
-abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_\<^sup>=)" [1000] 999)
+abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (\<open>(_\<^sup>=)\<close> [1000] 999)
where "r\<^sup>= \<equiv> r \<union> Id"
-abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_\<^sup>=\<^sup>=)" [1000] 1000)
+abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(_\<^sup>=\<^sup>=)\<close> [1000] 1000)
where "r\<^sup>=\<^sup>= \<equiv> sup r (=)"
notation (ASCII)
- rtrancl ("(_^*)" [1000] 999) and
- trancl ("(_^+)" [1000] 999) and
- reflcl ("(_^=)" [1000] 999) and
- rtranclp ("(_^**)" [1000] 1000) and
- tranclp ("(_^++)" [1000] 1000) and
- reflclp ("(_^==)" [1000] 1000)
+ rtrancl (\<open>(_^*)\<close> [1000] 999) and
+ trancl (\<open>(_^+)\<close> [1000] 999) and
+ reflcl (\<open>(_^=)\<close> [1000] 999) and
+ rtranclp (\<open>(_^**)\<close> [1000] 1000) and
+ tranclp (\<open>(_^++)\<close> [1000] 1000) and
+ reflclp (\<open>(_^==)\<close> [1000] 1000)
subsection \<open>Reflexive closure\<close>
--- a/src/HOL/Typerep.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Typerep.thy Mon Sep 23 13:32:38 2024 +0200
@@ -18,7 +18,7 @@
end
syntax
- "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))")
+ "_TYPEREP" :: "type => logic" (\<open>(1TYPEREP/(1'(_')))\<close>)
syntax_consts
"_TYPEREP" \<rightleftharpoons> typerep
--- a/src/HOL/Vector_Spaces.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Vector_Spaces.thy Mon Sep 23 13:32:38 2024 +0200
@@ -40,7 +40,7 @@
qed
locale vector_space =
- fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
+ fixes scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*s\<close> 75)
assumes vector_space_assms:\<comment> \<open>re-stating the assumptions of \<open>module\<close> instead of extending \<open>module\<close>
allows us to rewrite in the sublocale.\<close>
"a *s (x + y) = a *s x + a *s y"
@@ -52,8 +52,8 @@
unfolding module_def vector_space_def ..
locale linear = vs1: vector_space s1 + vs2: vector_space s2 + module_hom s1 s2 f
- for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
- and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
+ for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*a\<close> 75)
+ and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr \<open>*b\<close> 75)
and f :: "'b \<Rightarrow> 'c"
lemma module_hom_iff_linear: "module_hom s1 s2 f \<longleftrightarrow> linear s1 s2 f"
@@ -593,8 +593,8 @@
end
locale vector_space_pair = vs1: vector_space s1 + vs2: vector_space s2
- for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
- and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
+ for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*a\<close> 75)
+ and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr \<open>*b\<close> 75)
begin
context fixes f assumes "linear s1 s2 f" begin
@@ -1357,9 +1357,9 @@
locale finite_dimensional_vector_space_pair_1 =
vs1: finite_dimensional_vector_space s1 B1 + vs2: vector_space s2
- for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
+ for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*a\<close> 75)
and B1 :: "'b set"
- and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
+ and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr \<open>*b\<close> 75)
begin
sublocale vector_space_pair s1 s2 by unfold_locales
@@ -1405,9 +1405,9 @@
locale finite_dimensional_vector_space_pair =
vs1: finite_dimensional_vector_space s1 B1 + vs2: finite_dimensional_vector_space s2 B2
- for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*a" 75)
+ for s1 :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr \<open>*a\<close> 75)
and B1 :: "'b set"
- and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr "*b" 75)
+ and s2 :: "'a::field \<Rightarrow> 'c::ab_group_add \<Rightarrow> 'c" (infixr \<open>*b\<close> 75)
and B2 :: "'c set"
begin
--- a/src/HOL/Wellfounded.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Wellfounded.thy Mon Sep 23 13:32:38 2024 +0200
@@ -1121,7 +1121,7 @@
subsubsection \<open>Lexicographic combinations\<close>
definition lex_prod :: "('a \<times>'a) set \<Rightarrow> ('b \<times> 'b) set \<Rightarrow> (('a \<times> 'b) \<times> ('a \<times> 'b)) set"
- (infixr "<*lex*>" 80)
+ (infixr \<open><*lex*>\<close> 80)
where "ra <*lex*> rb = {((a, b), (a', b')). (a, a') \<in> ra \<or> a = a' \<and> (b, b') \<in> rb}"
lemma in_lex_prod[simp]: "((a, b), (a', b')) \<in> r <*lex*> s \<longleftrightarrow> (a, a') \<in> r \<or> a = a' \<and> (b, b') \<in> s"
@@ -1200,7 +1200,7 @@
text \<open>lexicographic combinations with measure functions\<close>
-definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
+definition mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr \<open><*mlex*>\<close> 80)
where "f <*mlex*> R = inv_image (less_than <*lex*> R) (\<lambda>x. (f x, x))"
lemma
--- a/src/HOL/Zorn.thy Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Zorn.thy Mon Sep 23 13:32:38 2024 +0200
@@ -19,10 +19,10 @@
text \<open>Let \<open>P\<close> be a binary predicate on the set \<open>A\<close>.\<close>
locale pred_on =
fixes A :: "'a set"
- and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubset>" 50)
+ and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>\<sqsubset>\<close> 50)
begin
-abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
+abbreviation Peq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix \<open>\<sqsubseteq>\<close> 50)
where "x \<sqsubseteq> y \<equiv> P\<^sup>=\<^sup>= x y"
text \<open>A chain is a totally ordered subset of \<open>A\<close>.\<close>
@@ -33,7 +33,7 @@
We call a chain that is a proper superset of some set \<open>X\<close>,
but not necessarily a chain itself, a superchain of \<open>X\<close>.
\<close>
-abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix "<c" 50)
+abbreviation superchain :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infix \<open><c\<close> 50)
where "X <c C \<equiv> chain C \<and> X \<subset> C"
text \<open>A maximal chain is a chain that does not have a superchain.\<close>
@@ -80,7 +80,7 @@
We build a set \<^term>\<open>\<C>\<close> that is closed under applications
of \<^term>\<open>suc\<close> and contains the union of all its subsets.
\<close>
-inductive_set suc_Union_closed ("\<C>")
+inductive_set suc_Union_closed (\<open>\<C>\<close>)
where
suc: "X \<in> \<C> \<Longrightarrow> suc X \<in> \<C>"
| Union [unfolded Pow_iff]: "X \<in> Pow \<C> \<Longrightarrow> \<Union>X \<in> \<C>"
@@ -315,7 +315,7 @@
qed
text \<open>Make notation \<^term>\<open>\<C>\<close> available again.\<close>
-no_notation suc_Union_closed ("\<C>")
+no_notation suc_Union_closed (\<open>\<C>\<close>)
lemma chain_extend: "chain C \<Longrightarrow> z \<in> A \<Longrightarrow> \<forall>x\<in>C. x \<sqsubseteq> z \<Longrightarrow> chain ({z} \<union> C)"
unfolding chain_def by blast
@@ -421,7 +421,7 @@
text \<open>Relate old to new definitions.\<close>
-definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^sub>\<subseteq>") (* Define globally? In Set.thy? *)
+definition chain_subset :: "'a set set \<Rightarrow> bool" (\<open>chain\<^sub>\<subseteq>\<close>) (* Define globally? In Set.thy? *)
where "chain\<^sub>\<subseteq> C \<longleftrightarrow> (\<forall>A\<in>C. \<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A)"
definition chains :: "'a set set \<Rightarrow> 'a set set set"
@@ -621,7 +621,7 @@
where "init_seg_of = {(r, s). r \<subseteq> s \<and> (\<forall>a b c. (a, b) \<in> s \<and> (b, c) \<in> r \<longrightarrow> (a, b) \<in> r)}"
abbreviation initial_segment_of_syntax :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"
- (infix "initial'_segment'_of" 55)
+ (infix \<open>initial'_segment'_of\<close> 55)
where "r initial_segment_of s \<equiv> (r, s) \<in> init_seg_of"
lemma refl_on_init_seg_of [simp]: "r initial_segment_of r"