--- a/src/CCL/CCL.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/CCL.thy Fri Sep 20 23:37:00 2024 +0200
@@ -35,7 +35,7 @@
(*** Term Formers ***)
true :: "i"
false :: "i"
- pair :: "[i,i]\<Rightarrow>i" (\<open>(1<_,/_>)\<close>)
+ pair :: "[i,i]\<Rightarrow>i" (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
lambda :: "(i\<Rightarrow>i)\<Rightarrow>i" (binder \<open>lam \<close> 55)
"case" :: "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
"apply" :: "[i,i]\<Rightarrow>i" (infixl \<open>`\<close> 56)
--- a/src/CCL/Set.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Set.thy Fri Sep 20 23:37:00 2024 +0200
@@ -18,7 +18,7 @@
and set_extension: "A = B \<longleftrightarrow> (ALL x. x:A \<longleftrightarrow> x:B)"
syntax
- "_Coll" :: "[idt, o] \<Rightarrow> 'a set" (\<open>(1{_./ _})\<close>)
+ "_Coll" :: "[idt, o] \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
syntax_consts
"_Coll" == Collect
translations
@@ -50,8 +50,8 @@
where "Bex(A, P) == EX x. x:A \<and> P(x)"
syntax
- "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" (\<open>(ALL _:_./ _)\<close> [0, 0, 0] 10)
- "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" (\<open>(EX _:_./ _)\<close> [0, 0, 0] 10)
+ "_Ball" :: "[idt, 'a set, o] \<Rightarrow> o" (\<open>(\<open>notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> [0, 0, 0] 10)
+ "_Bex" :: "[idt, 'a set, o] \<Rightarrow> o" (\<open>(\<open>notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> [0, 0, 0] 10)
syntax_consts
"_Ball" == Ball and
"_Bex" == Bex
@@ -127,8 +127,8 @@
where "UNION(A, B) == {y. EX x:A. y: B(x)}"
syntax
- "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" (\<open>(INT _:_./ _)\<close> [0, 0, 0] 10)
- "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" (\<open>(UN _:_./ _)\<close> [0, 0, 0] 10)
+ "_INTER" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" (\<open>(\<open>notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> [0, 0, 0] 10)
+ "_UNION" :: "[idt, 'a set, 'b set] \<Rightarrow> 'b set" (\<open>(\<open>notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> [0, 0, 0] 10)
syntax_consts
"_INTER" == INTER and
"_UNION" == UNION
--- a/src/CCL/Term.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Term.thy Fri Sep 20 23:37:00 2024 +0200
@@ -12,7 +12,8 @@
definition one :: "i"
where "one == true"
-definition "if" :: "[i,i,i]\<Rightarrow>i" (\<open>(3if _/ then _/ else _)\<close> [0,0,60] 60)
+definition "if" :: "[i,i,i]\<Rightarrow>i"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix if then else\<close>\<close>if _/ then _/ else _)\<close> [0,0,60] 60)
where "if b then t else u == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
definition inl :: "i\<Rightarrow>i"
@@ -48,7 +49,8 @@
definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" (\<open>(3let _ be _/ in _)\<close> [0,0,60] 60)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60)
syntax_consts "_let1" == let1
translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
@@ -65,9 +67,12 @@
\<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
syntax
- "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i" (\<open>(3letrec _ _ be _/ in _)\<close> [0,0,0,60] 60)
- "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" (\<open>(3letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
- "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" (\<open>(3letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
+ "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ be _/ in _)\<close> [0,0,0,60] 60)
+ "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60)
+ "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60)
syntax_consts
"_letrec" == letrec and
"_letrec2" == letrec2 and
@@ -143,7 +148,7 @@
definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
-definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i" (\<open>(_ ^ _ ` _)\<close> [56,56,56] 56)
+definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i" (\<open>(\<open>notation=\<open>mixfix napply\<close>\<close>_ ^ _ ` _)\<close> [56,56,56] 56)
where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
lemmas simp_can_defs = one_def inl_def inr_def
--- a/src/CCL/Trancl.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Trancl.thy Fri Sep 20 23:37:00 2024 +0200
@@ -18,10 +18,10 @@
definition relcomp :: "[i set,i set] \<Rightarrow> i set" (infixr \<open>O\<close> 60) (*composition of relations*)
where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
-definition rtrancl :: "i set \<Rightarrow> i set" (\<open>(_^*)\<close> [100] 100)
+definition rtrancl :: "i set \<Rightarrow> i set" (\<open>(\<open>notation=\<open>postfix ^*\<close>\<close>_^*)\<close> [100] 100)
where "r^* == lfp(\<lambda>s. id Un (r O s))"
-definition trancl :: "i set \<Rightarrow> i set" (\<open>(_^+)\<close> [100] 100)
+definition trancl :: "i set \<Rightarrow> i set" (\<open>(\<open>notation=\<open>postfix ^+\<close>\<close>_^+)\<close> [100] 100)
where "r^+ == r O rtrancl(r)"
--- a/src/CCL/Type.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CCL/Type.thy Fri Sep 20 23:37:00 2024 +0200
@@ -13,7 +13,7 @@
where "Subtype(A, P) == {x. x:A \<and> P(x)}"
syntax
- "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" (\<open>(1{_: _ ./ _})\<close>)
+ "_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
syntax_consts
"_Subtype" == Subtype
translations
@@ -35,10 +35,10 @@
where "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
syntax
- "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" (\<open>(3PROD _:_./ _)\<close> [0,0,60] 60)
- "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" (\<open>(3SUM _:_./ _)\<close> [0,0,60] 60)
- "_arrow" :: "[i set, i set] \<Rightarrow> i set" (\<open>(_ ->/ _)\<close> [54, 53] 53)
- "_star" :: "[i set, i set] \<Rightarrow> i set" (\<open>(_ */ _)\<close> [56, 55] 55)
+ "_Pi" :: "[idt, i set, i set] \<Rightarrow> i set" (\<open>(\<open>indent=3 notation=\<open>binder PROD:\<close>\<close>PROD _:_./ _)\<close> [0,0,60] 60)
+ "_Sigma" :: "[idt, i set, i set] \<Rightarrow> i set" (\<open>(\<open>indent=3 notation=\<open>binder SUM:\<close>\<close>SUM _:_./ _)\<close> [0,0,60] 60)
+ "_arrow" :: "[i set, i set] \<Rightarrow> i set" (\<open>(\<open>notation=\<open>infix ->\<close>\<close>_ ->/ _)\<close> [54, 53] 53)
+ "_star" :: "[i set, i set] \<Rightarrow> i set" (\<open>(\<open>notation=\<open>infix *\<close>\<close>_ */ _)\<close> [56, 55] 55)
syntax_consts
"_Pi" "_arrow" \<rightleftharpoons> Pi and
"_Sigma" "_star" \<rightleftharpoons> Sigma
@@ -73,7 +73,7 @@
definition TEx :: "(i set \<Rightarrow> i set) \<Rightarrow> i set" (binder \<open>TEX \<close> 55)
where "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
-definition Lift :: "i set \<Rightarrow> i set" (\<open>(3[_])\<close>)
+definition Lift :: "i set \<Rightarrow> i set" (\<open>(\<open>indent=3 notation=\<open>mixfix Lift\<close>\<close>[_])\<close>)
where "[A] == A Un {bot}"
definition SPLIT :: "[i, [i, i] \<Rightarrow> i set] \<Rightarrow> i set"
--- a/src/CTT/CTT.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/CTT/CTT.thy Fri Sep 20 23:37:00 2024 +0200
@@ -18,10 +18,10 @@
consts
\<comment> \<open>Judgments\<close>
- Type :: "t \<Rightarrow> prop" (\<open>(_ type)\<close> [10] 5)
- Eqtype :: "[t,t]\<Rightarrow>prop" (\<open>(_ =/ _)\<close> [10,10] 5)
- Elem :: "[i, t]\<Rightarrow>prop" (\<open>(_ /: _)\<close> [10,10] 5)
- Eqelem :: "[i,i,t]\<Rightarrow>prop" (\<open>(_ =/ _ :/ _)\<close> [10,10,10] 5)
+ Type :: "t \<Rightarrow> prop" (\<open>(\<open>notation=\<open>postfix Type\<close>\<close>_ type)\<close> [10] 5)
+ Eqtype :: "[t,t]\<Rightarrow>prop" (\<open>(\<open>notation=\<open>infix Eqtype\<close>\<close>_ =/ _)\<close> [10,10] 5)
+ Elem :: "[i, t]\<Rightarrow>prop" (\<open>(\<open>notation=\<open>infix Elem\<close>\<close>_ /: _)\<close> [10,10] 5)
+ Eqelem :: "[i,i,t]\<Rightarrow>prop" (\<open>(\<open>notation=\<open>mixfix Eqelem\<close>\<close>_ =/ _ :/ _)\<close> [10,10,10] 5)
Reduce :: "[i,i]\<Rightarrow>prop" (\<open>Reduce[_,_]\<close>)
\<comment> \<open>Types for truth values\<close>
F :: "t"
@@ -40,7 +40,7 @@
"when" :: "[i, i\<Rightarrow>i, i\<Rightarrow>i]\<Rightarrow>i"
\<comment> \<open>General sum and binary product\<close>
Sum :: "[t, i\<Rightarrow>t]\<Rightarrow>t"
- pair :: "[i,i]\<Rightarrow>i" (\<open>(1<_,/_>)\<close>)
+ pair :: "[i,i]\<Rightarrow>i" (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
fst :: "i\<Rightarrow>i"
snd :: "i\<Rightarrow>i"
split :: "[i, [i,i]\<Rightarrow>i] \<Rightarrow>i"
@@ -56,8 +56,8 @@
must be introduced after the judgment forms.\<close>
syntax
- "_PROD" :: "[idt,t,t]\<Rightarrow>t" (\<open>(3\<Prod>_:_./ _)\<close> 10)
- "_SUM" :: "[idt,t,t]\<Rightarrow>t" (\<open>(3\<Sum>_:_./ _)\<close> 10)
+ "_PROD" :: "[idt,t,t]\<Rightarrow>t" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_:_./ _)\<close> 10)
+ "_SUM" :: "[idt,t,t]\<Rightarrow>t" (\<open>(\<open>indent=3 notation=\<open>binder \<Sum>\<close>\<close>\<Sum>_:_./ _)\<close> 10)
syntax_consts
"_PROD" \<rightleftharpoons> Prod and
"_SUM" \<rightleftharpoons> Sum
--- a/src/Cube/Cube.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Cube/Cube.thy Fri Sep 20 23:37:00 2024 +0200
@@ -29,15 +29,15 @@
nonterminal context' and typing'
syntax
- "_Trueprop" :: "[context', typing'] \<Rightarrow> prop" (\<open>(_/ \<turnstile> _)\<close>)
- "_Trueprop1" :: "typing' \<Rightarrow> prop" (\<open>(_)\<close>)
+ "_Trueprop" :: "[context', typing'] \<Rightarrow> prop" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>_/ \<turnstile> _)\<close>)
+ "_Trueprop1" :: "typing' \<Rightarrow> prop" (\<open>(\<open>notation=\<open>prefix Trueprop\<close>\<close>_)\<close>)
"" :: "id \<Rightarrow> context'" (\<open>_\<close>)
"" :: "var \<Rightarrow> context'" (\<open>_\<close>)
"_MT_context" :: "context'" (\<open>\<close>)
"_Context" :: "[typing', context'] \<Rightarrow> context'" (\<open>_ _\<close>)
- "_Has_type" :: "[term, term] \<Rightarrow> typing'" (\<open>(_:/ _)\<close> [0, 0] 5)
- "_Lam" :: "[idt, term, term] \<Rightarrow> term" (\<open>(3\<^bold>\<lambda>_:_./ _)\<close> [0, 0, 0] 10)
- "_Pi" :: "[idt, term, term] \<Rightarrow> term" (\<open>(3\<Prod>_:_./ _)\<close> [0, 0] 10)
+ "_Has_type" :: "[term, term] \<Rightarrow> typing'" (\<open>(\<open>notation=\<open>infix Has_Type\<close>\<close>_:/ _)\<close> [0, 0] 5)
+ "_Lam" :: "[idt, term, term] \<Rightarrow> term" (\<open>(\<open>indent=3 notation=\<open>binder \<^bold>\<lambda>\<close>\<close>\<^bold>\<lambda>_:_./ _)\<close> [0, 0, 0] 10)
+ "_Pi" :: "[idt, term, term] \<Rightarrow> term" (\<open>(\<open>indent=3 notation=\<open>binder \<Prod>\<close>\<close>\<Prod>_:_./ _)\<close> [0, 0] 10)
"_arrow" :: "[term, term] \<Rightarrow> term" (infixr \<open>\<rightarrow>\<close> 10)
syntax_consts
"_Trueprop" \<rightleftharpoons> Trueprop and
--- a/src/FOL/IFOL.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/FOL/IFOL.thy Fri Sep 20 23:37:00 2024 +0200
@@ -101,7 +101,7 @@
abbreviation not_equal :: \<open>['a, 'a] \<Rightarrow> o\<close> (infixl \<open>\<noteq>\<close> 50)
where \<open>x \<noteq> y \<equiv> \<not> (x = y)\<close>
-syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" (\<open>(2\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
+syntax "_Uniq" :: "pttrn \<Rightarrow> o \<Rightarrow> o" (\<open>(\<open>indent=2 notation=\<open>binder \<exists>\<^sub>\<le>\<^sub>1\<close>\<close>\<exists>\<^sub>\<le>\<^sub>1 _./ _)\<close> [0, 10] 10)
syntax_consts "_Uniq" \<rightleftharpoons> Uniq
translations "\<exists>\<^sub>\<le>\<^sub>1x. P" \<rightleftharpoons> "CONST Uniq (\<lambda>x. P)"
@@ -743,10 +743,10 @@
where \<open>Let(s, f) \<equiv> f(s)\<close>
syntax
- "_bind" :: \<open>[pttrn, 'a] => letbind\<close> (\<open>(2_ =/ _)\<close> 10)
+ "_bind" :: \<open>[pttrn, 'a] => letbind\<close> (\<open>(\<open>indent=2 notation=\<open>infix letbind\<close>\<close>_ =/ _)\<close> 10)
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
- "_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(let (_)/ in (_))\<close> 10)
+ "_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
syntax_consts "_Let" \<rightleftharpoons> Let
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
--- a/src/FOLP/IFOLP.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/FOLP/IFOLP.thy Fri Sep 20 23:37:00 2024 +0200
@@ -23,7 +23,7 @@
consts
(*** Judgements ***)
Proof :: "[o,p]=>prop"
- EqProof :: "[p,p,o]=>prop" (\<open>(3_ /= _ :/ _)\<close> [10,10,10] 5)
+ EqProof :: "[p,p,o]=>prop" (\<open>(\<open>indent=3 notation=\<open>mixfix EqProof\<close>\<close>_ /= _ :/ _)\<close> [10,10,10] 5)
(*** Logical Connectives -- Type Formers ***)
eq :: "['a,'a] => o" (infixl \<open>=\<close> 50)
@@ -44,7 +44,7 @@
contr :: "p=>p"
fst :: "p=>p"
snd :: "p=>p"
- pair :: "[p,p]=>p" (\<open>(1<_,/_>)\<close>)
+ pair :: "[p,p]=>p" (\<open>(\<open>indent=1 notation=\<open>mixfix pair\<close>\<close><_,/_>)\<close>)
split :: "[p, [p,p]=>p] =>p"
inl :: "p=>p"
inr :: "p=>p"
@@ -53,14 +53,14 @@
App :: "[p,p]=>p" (infixl \<open>`\<close> 60)
alll :: "['a=>p]=>p" (binder \<open>all \<close> 55)
app :: "[p,'a]=>p" (infixl \<open>^\<close> 55)
- exists :: "['a,p]=>p" (\<open>(1[_,/_])\<close>)
+ exists :: "['a,p]=>p" (\<open>(\<open>indent=1 notation=\<open>mixfix exists\<close>\<close>[_,/_])\<close>)
xsplit :: "[p,['a,p]=>p]=>p"
ideq :: "'a=>p"
idpeel :: "[p,'a=>p]=>p"
nrm :: p
NRM :: p
-syntax "_Proof" :: "[p,o]=>prop" (\<open>(_ /: _)\<close> [51, 10] 5)
+syntax "_Proof" :: "[p,o]=>prop" (\<open>(\<open>notation=\<open>infix Proof\<close>\<close>_ /: _)\<close> [51, 10] 5)
parse_translation \<open>
let fun proof_tr [p, P] = Syntax.const \<^const_syntax>\<open>Proof\<close> $ P $ p
--- a/src/LCF/LCF.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/LCF/LCF.thy Fri Sep 20 23:37:00 2024 +0200
@@ -39,8 +39,8 @@
WHEN :: "['a\<Rightarrow>'c, 'b\<Rightarrow>'c, 'a+'b] \<Rightarrow> 'c"
adm :: "('a \<Rightarrow> o) \<Rightarrow> o"
VOID :: "void" (\<open>'(')\<close>)
- PAIR :: "['a,'b] \<Rightarrow> 'a*'b" (\<open>(1<_,/_>)\<close> [0,0] 100)
- COND :: "[tr,'a,'a] \<Rightarrow> 'a" (\<open>(_ \<Rightarrow>/ (_ |/ _))\<close> [60,60,60] 60)
+ PAIR :: "['a,'b] \<Rightarrow> 'a*'b" (\<open>(\<open>indent=1 notation=\<open>mixfix PAIR\<close>\<close><_,/_>)\<close> [0,0] 100)
+ COND :: "[tr,'a,'a] \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix COND\<close>\<close>_ \<Rightarrow>/ (_ |/ _))\<close> [60,60,60] 60)
less :: "['a,'a] \<Rightarrow> o" (infixl \<open><<\<close> 50)
axiomatization where
--- a/src/Sequents/ILL.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/ILL.thy Fri Sep 20 23:37:00 2024 +0200
@@ -29,8 +29,8 @@
PromAux :: "three_seqi"
syntax
- "_Trueprop" :: "single_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
- "_Context" :: "two_seqe" (\<open>((_)/ :=: (_))\<close> [6,6] 5)
+ "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+ "_Context" :: "two_seqe" (\<open>(\<open>notation=\<open>infix Context\<close>\<close>(_)/ :=: (_))\<close> [6,6] 5)
"_PromAux" :: "three_seqe" (\<open>promaux {_||_||_}\<close>)
parse_translation \<open>
--- a/src/Sequents/LK0.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/LK0.thy Fri Sep 20 23:37:00 2024 +0200
@@ -34,7 +34,7 @@
Ex :: "('a \<Rightarrow> o) \<Rightarrow> o" (binder \<open>\<exists>\<close> 10)
syntax
- "_Trueprop" :: "two_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
+ "_Trueprop" :: "two_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
parse_translation \<open>[(\<^syntax_const>\<open>_Trueprop\<close>, K (two_seq_tr \<^const_syntax>\<open>Trueprop\<close>))]\<close>
print_translation \<open>[(\<^const_syntax>\<open>Trueprop\<close>, K (two_seq_tr' \<^syntax_const>\<open>_Trueprop\<close>))]\<close>
@@ -104,7 +104,7 @@
The: "\<lbrakk>$H \<turnstile> $E, P(a), $F; \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
$H \<turnstile> $E, P(THE x. P(x)), $F"
-definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" (\<open>(if (_)/ then (_)/ else (_))\<close> 10)
+definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" (\<open>(\<open>notation=\<open>mixfix if then else\<close>\<close>if (_)/ then (_)/ else (_))\<close> 10)
where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
--- a/src/ZF/Finite.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Finite.thy Fri Sep 20 23:37:00 2024 +0200
@@ -19,7 +19,7 @@
consts
Fin :: "i\<Rightarrow>i"
- FiniteFun :: "[i,i]\<Rightarrow>i" (\<open>(_ -||>/ _)\<close> [61, 60] 60)
+ FiniteFun :: "[i,i]\<Rightarrow>i" (\<open>(\<open>notation=\<open>infix -||>\<close>\<close>_ -||>/ _)\<close> [61, 60] 60)
inductive
domains "Fin(A)" \<subseteq> "Pow(A)"
--- a/src/ZF/Induct/Multiset.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Fri Sep 20 23:37:00 2024 +0200
@@ -70,11 +70,11 @@
"msize(M) \<equiv> setsum(\<lambda>a. $# mcount(M,a), mset_of(M))"
abbreviation
- melem :: "[i,i] \<Rightarrow> o" (\<open>(_/ :# _)\<close> [50, 51] 50) where
+ melem :: "[i,i] \<Rightarrow> o" (\<open>(\<open>notation=\<open>infix :#\<close>\<close>_/ :# _)\<close> [50, 51] 50) where
"a :# M \<equiv> a \<in> mset_of(M)"
syntax
- "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{# _ \<in> _./ _#})\<close>)
+ "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
syntax_consts "_MColl" \<rightleftharpoons> MCollect
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
--- a/src/ZF/OrdQuant.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/OrdQuant.thy Fri Sep 20 23:37:00 2024 +0200
@@ -23,9 +23,9 @@
"OUnion(i,B) \<equiv> {z: \<Union>x\<in>i. B(x). Ord(i)}"
syntax
- "_oall" :: "[idt, i, o] \<Rightarrow> o" (\<open>(3\<forall>_<_./ _)\<close> 10)
- "_oex" :: "[idt, i, o] \<Rightarrow> o" (\<open>(3\<exists>_<_./ _)\<close> 10)
- "_OUNION" :: "[idt, i, i] \<Rightarrow> i" (\<open>(3\<Union>_<_./ _)\<close> 10)
+ "_oall" :: "[idt, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<forall><\<close>\<close>\<forall>_<_./ _)\<close> 10)
+ "_oex" :: "[idt, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<exists><\<close>\<close>\<exists>_<_./ _)\<close> 10)
+ "_OUNION" :: "[idt, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder \<Union><\<close>\<close>\<Union>_<_./ _)\<close> 10)
syntax_consts
"_oall" \<rightleftharpoons> oall and
"_oex" \<rightleftharpoons> oex and
@@ -196,8 +196,8 @@
"rex(M, P) \<equiv> \<exists>x. M(x) \<and> P(x)"
syntax
- "_rall" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(3\<forall>_[_]./ _)\<close> 10)
- "_rex" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(3\<exists>_[_]./ _)\<close> 10)
+ "_rall" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>[]\<close>\<close>\<forall>_[_]./ _)\<close> 10)
+ "_rex" :: "[pttrn, i\<Rightarrow>o, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>[]\<close>\<close>\<exists>_[_]./ _)\<close> 10)
syntax_consts
"_rall" \<rightleftharpoons> rall and
"_rex" \<rightleftharpoons> rex
--- a/src/ZF/Order.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Order.thy Fri Sep 20 23:37:00 2024 +0200
@@ -49,7 +49,7 @@
{f \<in> A->B. \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longrightarrow> <f`x,f`y>:s}"
definition
- ord_iso :: "[i,i,i,i]\<Rightarrow>i" (\<open>(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51) (*Order isomorphisms*) where
+ ord_iso :: "[i,i,i,i]\<Rightarrow>i" (\<open>(\<open>notation=\<open>infix ord_iso\<close>\<close>\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)\<close> 51) (*Order isomorphisms*) where
"\<langle>A,r\<rangle> \<cong> \<langle>B,s\<rangle> \<equiv>
{f \<in> bij(A,B). \<forall>x\<in>A. \<forall>y\<in>A. \<langle>x,y\<rangle>:r \<longleftrightarrow> <f`x,f`y>:s}"
--- a/src/ZF/QPair.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/QPair.thy Fri Sep 20 23:37:00 2024 +0200
@@ -45,7 +45,7 @@
"QSigma(A,B) \<equiv> \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
syntax
- "_QSUM" :: "[idt, i, i] \<Rightarrow> i" (\<open>(3QSUM _ \<in> _./ _)\<close> 10)
+ "_QSUM" :: "[idt, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder QSUM\<in>\<close>\<close>QSUM _ \<in> _./ _)\<close> 10)
syntax_consts
"_QSUM" \<rightleftharpoons> QSigma
translations
--- a/src/ZF/Trancl.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/Trancl.thy Fri Sep 20 23:37:00 2024 +0200
@@ -37,11 +37,11 @@
\<langle>x,y\<rangle>: r \<longrightarrow> \<langle>y,z\<rangle>: r \<longrightarrow> \<langle>x,z\<rangle>: r"
definition
- rtrancl :: "i\<Rightarrow>i" (\<open>(_^*)\<close> [100] 100) (*refl/transitive closure*) where
+ rtrancl :: "i\<Rightarrow>i" (\<open>(\<open>notation=\<open>postfix ^*\<close>\<close>_^*)\<close> [100] 100) (*refl/transitive closure*) where
"r^* \<equiv> lfp(field(r)*field(r), \<lambda>s. id(field(r)) \<union> (r O s))"
definition
- trancl :: "i\<Rightarrow>i" (\<open>(_^+)\<close> [100] 100) (*transitive closure*) where
+ trancl :: "i\<Rightarrow>i" (\<open>(\<open>notation=\<open>postfix ^+\<close>\<close>_^+)\<close> [100] 100) (*transitive closure*) where
"r^+ \<equiv> r O r^*"
definition
--- a/src/ZF/UNITY/Follows.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Follows.thy Fri Sep 20 23:37:00 2024 +0200
@@ -39,7 +39,7 @@
abbreviation
Follows' :: "[i\<Rightarrow>i, i\<Rightarrow>i, i, i] \<Rightarrow> i"
- (\<open>(_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60) where
+ (\<open>(\<open>notation=\<open>mixfix Fols Wrt\<close>\<close>_ /Fols _ /Wrt (_ /'/ _))\<close> [60, 0, 0, 60] 60) where
"f Fols g Wrt r/A \<equiv> Follows(A,r,f,g)"
--- a/src/ZF/UNITY/Guar.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Guar.thy Fri Sep 20 23:37:00 2024 +0200
@@ -77,13 +77,13 @@
"welldef \<equiv> {F \<in> program. Init(F) \<noteq> 0}"
definition
- refines :: "[i, i, i] \<Rightarrow> o" (\<open>(3_ refines _ wrt _)\<close> [10,10,10] 10) where
+ refines :: "[i, i, i] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>mixfix refines wrt\<close>\<close>_ refines _ wrt _)\<close> [10,10,10] 10) where
"G refines F wrt X \<equiv>
\<forall>H \<in> program. (F ok H \<and> G ok H \<and> F \<squnion> H \<in> welldef \<inter> X)
\<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)"
definition
- iso_refines :: "[i,i, i] \<Rightarrow> o" (\<open>(3_ iso'_refines _ wrt _)\<close> [10,10,10] 10) where
+ iso_refines :: "[i,i, i] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>mixfix iso_refines wrt\<close>\<close>_ iso'_refines _ wrt _)\<close> [10,10,10] 10) where
"G iso_refines F wrt X \<equiv> F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X"
--- a/src/ZF/UNITY/Increasing.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Increasing.thy Fri Sep 20 23:37:00 2024 +0200
@@ -23,7 +23,7 @@
(\<forall>x \<in> state. f(x):A)}"
abbreviation (input)
- IncWrt :: "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60) where
+ IncWrt :: "[i\<Rightarrow>i, i, i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix IncreasingWrt\<close>\<close>_ IncreasingWrt _ '/ _)\<close> [60, 0, 60] 60) where
"f IncreasingWrt r/A \<equiv> Increasing[A](r,f)"
--- a/src/ZF/UNITY/Union.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/UNITY/Union.thy Fri Sep 20 23:37:00 2024 +0200
@@ -41,8 +41,8 @@
SKIP \<in> X \<and> (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) \<longrightarrow> G \<in> X)"
syntax
- "_JOIN1" :: "[pttrns, i] \<Rightarrow> i" (\<open>(3\<Squnion>_./ _)\<close> 10)
- "_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Squnion>_ \<in> _./ _)\<close> 10)
+ "_JOIN1" :: "[pttrns, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> 10)
+ "_JOIN" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<in>\<close>\<close>\<Squnion>_ \<in> _./ _)\<close> 10)
syntax_consts
"_JOIN1" "_JOIN" == JOIN
translations
--- a/src/ZF/ZF.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ZF.thy Fri Sep 20 23:37:00 2024 +0200
@@ -7,14 +7,14 @@
subsection\<open>Iteration of the function \<^term>\<open>F\<close>\<close>
-consts iterates :: "[i\<Rightarrow>i,i,i] \<Rightarrow> i" (\<open>(_^_ '(_'))\<close> [60,1000,1000] 60)
+consts iterates :: "[i\<Rightarrow>i,i,i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix iterates\<close>\<close>_^_ '(_'))\<close> [60,1000,1000] 60)
primrec
"F^0 (x) = x"
"F^(succ(n)) (x) = F(F^n (x))"
definition
- iterates_omega :: "[i\<Rightarrow>i,i] \<Rightarrow> i" (\<open>(_^\<omega> '(_'))\<close> [60,1000] 60) where
+ iterates_omega :: "[i\<Rightarrow>i,i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix iterates_omega\<close>\<close>_^\<omega> '(_'))\<close> [60,1000] 60) where
"F^\<omega> (x) \<equiv> \<Union>n\<in>nat. F^n (x)"
lemma iterates_triv:
--- a/src/ZF/ZF_Base.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ZF_Base.thy Fri Sep 20 23:37:00 2024 +0200
@@ -36,8 +36,8 @@
where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
syntax
- "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
- "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
+ "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<in>\<close>\<close>\<forall>_\<in>_./ _)\<close> 10)
+ "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder \<exists>\<in>\<close>\<close>\<exists>_\<in>_./ _)\<close> 10)
syntax_consts
"_Ball" \<rightleftharpoons> Ball and
"_Bex" \<rightleftharpoons> Bex
@@ -55,7 +55,7 @@
where "Replace(A,P) \<equiv> PrimReplace(A, \<lambda>x y. (\<exists>!z. P(x,z)) \<and> P(x,y))"
syntax
- "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _, _})\<close>)
+ "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
syntax_consts
"_Replace" \<rightleftharpoons> Replace
translations
@@ -68,7 +68,7 @@
where "RepFun(A,f) \<equiv> {y . x\<in>A, y=f(x)}"
syntax
- "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
+ "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
syntax_consts
"_RepFun" \<rightleftharpoons> RepFun
translations
@@ -80,7 +80,7 @@
where "Collect(A,P) \<equiv> {y . x\<in>A, x=y \<and> P(x)}"
syntax
- "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ \<in> _ ./ _})\<close>)
+ "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_ \<in> _ ./ _})\<close>)
syntax_consts
"_Collect" \<rightleftharpoons> Collect
translations
@@ -93,8 +93,8 @@
where "\<Inter>(A) \<equiv> { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
syntax
- "_UNION" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
- "_INTER" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
+ "_UNION" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder \<Union>\<in>\<close>\<close>\<Union>_\<in>_./ _)\<close> 10)
+ "_INTER" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder \<Inter>\<in>\<close>\<close>\<Inter>_\<in>_./ _)\<close> 10)
syntax_consts
"_UNION" == Union and
"_INTER" == Inter
@@ -169,7 +169,7 @@
definition The :: "(i \<Rightarrow> o) \<Rightarrow> i" (binder \<open>THE \<close> 10)
where the_def: "The(P) \<equiv> \<Union>({y . x \<in> {0}, P(y)})"
-definition If :: "[o, i, i] \<Rightarrow> i" (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10)
+definition If :: "[o, i, i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>mixfix if then else\<close>\<close>if (_)/ then (_)/ else (_))\<close> [10] 10)
where if_def: "if P then a else b \<equiv> THE z. P \<and> z=a | \<not>P \<and> z=b"
abbreviation (input)
@@ -272,9 +272,9 @@
(* binder syntax *)
syntax
- "_PROD" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
- "_SUM" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
- "_lam" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
+ "_PROD" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>mixfix \<Prod>\<in>\<close>\<close>\<Prod>_\<in>_./ _)\<close> 10)
+ "_SUM" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>mixfix \<Sum>\<in>\<close>\<close>\<Sum>_\<in>_./ _)\<close> 10)
+ "_lam" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>mixfix \<lambda>\<in>\<close>\<close>\<lambda>_\<in>_./ _)\<close> 10)
syntax_consts
"_PROD" == Pi and
"_SUM" == Sigma and
@@ -297,16 +297,16 @@
not_mem (infixl \<open>\<not>:\<close> 50)
syntax (ASCII)
- "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3ALL _:_./ _)\<close> 10)
- "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(3EX _:_./ _)\<close> 10)
- "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(1{_: _ ./ _})\<close>)
- "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(1{_ ./ _: _, _})\<close>)
- "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(1{_ ./ _: _})\<close> [51,0,51])
- "_UNION" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3UN _:_./ _)\<close> 10)
- "_INTER" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3INT _:_./ _)\<close> 10)
- "_PROD" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3PROD _:_./ _)\<close> 10)
- "_SUM" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3SUM _:_./ _)\<close> 10)
- "_lam" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(3lam _:_./ _)\<close> 10)
+ "_Ball" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> 10)
+ "_Bex" :: "[pttrn, i, o] \<Rightarrow> o" (\<open>(\<open>indent=3 notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> 10)
+ "_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_: _ ./ _})\<close>)
+ "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _: _, _})\<close>)
+ "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _: _})\<close> [51,0,51])
+ "_UNION" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> 10)
+ "_INTER" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> 10)
+ "_PROD" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder PROD:\<close>\<close>PROD _:_./ _)\<close> 10)
+ "_SUM" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder SUM:\<close>\<close>SUM _:_./ _)\<close> 10)
+ "_lam" :: "[pttrn, i, i] \<Rightarrow> i" (\<open>(\<open>indent=3 notation=\<open>binder lam:\<close>\<close>lam _:_./ _)\<close> 10)
"_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open><(_,/ _)>\<close>)
"_pattern" :: "patterns \<Rightarrow> pttrn" (\<open><_>\<close>)
--- a/src/ZF/ex/Ring.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/ex/Ring.thy Fri Sep 20 23:37:00 2024 +0200
@@ -46,7 +46,7 @@
"a_inv(R) \<equiv> m_inv (<carrier(R), add_field(R), zero(R), 0>)"
definition
- minus :: "[i,i,i] \<Rightarrow> i" (\<open>(_ \<ominus>\<index> _)\<close> [65,66] 65) where
+ minus :: "[i,i,i] \<Rightarrow> i" (\<open>(\<open>notation=\<open>infix \<ominus>\<close>\<close>_ \<ominus>\<index> _)\<close> [65,66] 65) where
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
locale abelian_monoid = fixes G (structure)
--- a/src/ZF/func.thy Fri Sep 20 23:36:33 2024 +0200
+++ b/src/ZF/func.thy Fri Sep 20 23:37:00 2024 +0200
@@ -448,7 +448,7 @@
nonterminal updbinds and updbind
syntax
- "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
+ "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)