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