# HG changeset patch # User wenzelm # Date 1727818570 -7200 # Node ID 49c04500c5f90154d6204ee356b9a185e7b37281 # Parent 2a8afc91ce9c5b4e235091256c8e125fd8bddbd8 more inner syntax markup: HOLCF; diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Tue Oct 01 23:36:10 2024 +0200 @@ -16,17 +16,17 @@ definition "cfun = {f::'a \ 'b. cont f}" -cpodef ('a, 'b) cfun (\(_ \/ _)\ [1, 0] 0) = "cfun :: ('a \ 'b) set" +cpodef ('a, 'b) cfun (\(\notation=\infix \\\_ \/ _)\ [1, 0] 0) = "cfun :: ('a \ 'b) set" by (auto simp: cfun_def intro: cont_const adm_cont) type_notation (ASCII) cfun (infixr \->\ 0) notation (ASCII) - Rep_cfun (\(_$/_)\ [999,1000] 999) + Rep_cfun (\(\notation=\infix $\\_$/_)\ [999,1000] 999) notation - Rep_cfun (\(_\/_)\ [999,1000] 999) + Rep_cfun (\(\notation=\infix \\\_\/_)\ [999,1000] 999) subsection \Syntax for continuous lambda abstraction\ @@ -47,10 +47,10 @@ text \Syntax for nested abstractions\ syntax (ASCII) - "_Lambda" :: "[cargs, logic] \ logic" (\(3LAM _./ _)\ [1000, 10] 10) + "_Lambda" :: "[cargs, logic] \ logic" (\(\indent=3 notation=\binder LAM\\LAM _./ _)\ [1000, 10] 10) syntax - "_Lambda" :: "[cargs, logic] \ logic" (\(3\ _./ _)\ [1000, 10] 10) + "_Lambda" :: "[cargs, logic] \ logic" (\(\indent=3 notation=\binder \\\\ _./ _)\ [1000, 10] 10) syntax_consts "_Lambda" \ Abs_cfun diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/ConvexPD.thy Tue Oct 01 23:36:10 2024 +0200 @@ -119,7 +119,7 @@ subsection \Type definition\ -typedef 'a convex_pd (\('(_')\)\) = +typedef 'a convex_pd (\(\notation=\postfix convex_pd\\'(_')\)\) = "{S::'a pd_basis set. convex_le.ideal S}" by (rule convex_le.ex_ideal) @@ -345,10 +345,7 @@ syntax "_convex_bind" :: "[logic, logic, logic] \ logic" - (\(3\\_\_./ _)\ [0, 0, 10] 10) - -syntax_consts - "_convex_bind" == convex_bind + (\(\indent=3 notation=\binder convex_bind\\\\_\_./ _)\ [0, 0, 10] 10) translations "\\x\xs. e" == "CONST convex_bind\xs\(\ x. e)" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/FOCUS/Fstream.thy --- a/src/HOL/HOLCF/FOCUS/Fstream.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Tue Oct 01 23:36:10 2024 +0200 @@ -29,16 +29,16 @@ "<> == \" abbreviation - fscons' :: "'a \ 'a fstream \ 'a fstream" (\(_\_)\ [66,65] 65) where + fscons' :: "'a \ 'a fstream \ 'a fstream" (\(\notation=\infix \\\_\_)\ [66,65] 65) where "a\s == fscons a\s" abbreviation - fsfilter' :: "'a set \ 'a fstream \ 'a fstream" (\(_\_)\ [64,63] 63) where + fsfilter' :: "'a set \ 'a fstream \ 'a fstream" (\(\notation=\infix \\\_\_)\ [64,63] 63) where "A\s == fsfilter A\s" notation (ASCII) - fscons' (\(_~>_)\ [66,65] 65) and - fsfilter' (\(_'(C')_)\ [64,63] 63) + fscons' (\(\notation=\infix ~>\\_~>_)\ [66,65] 65) and + fsfilter' (\(\notation=\infix (C)\\_'(C')_)\ [64,63] 63) lemma Def_maximal: "a = Def d \ a\b \ b = Def d" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/FOCUS/Fstreams.thy --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Tue Oct 01 23:36:10 2024 +0200 @@ -44,11 +44,11 @@ "<> == \" abbreviation - fsfilter' :: "'a set \ 'a fstream \ 'a fstream" (\(_\_)\ [64,63] 63) where + fsfilter' :: "'a set \ 'a fstream \ 'a fstream" (\(\notation=\infix \\\_\_)\ [64,63] 63) where "A\s == fsfilter A\s" notation (ASCII) - fsfilter' (\(_'(C')_)\ [64,63] 63) + fsfilter' (\(\notation=\infix (C)\\_'(C')_)\ [64,63] 63) lemma ft_fsingleton[simp]: "ft\() = Def a" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/IOA/Sequence.thy --- a/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/IOA/Sequence.thy Tue Oct 01 23:36:10 2024 +0200 @@ -63,7 +63,7 @@ UU \ UU | Def y \ (if P y then x ## (h \ xs) else h \ xs))))" -abbreviation Consq_syn (\(_/\_)\ [66, 65] 65) +abbreviation Consq_syn (\(\notation=\infix \\\_/\_)\ [66, 65] 65) where "a \ s \ Consq a \ s" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/IOA/TL.thy --- a/src/HOL/HOLCF/IOA/TL.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/IOA/TL.thy Tue Oct 01 23:36:10 2024 +0200 @@ -22,7 +22,7 @@ where "Init P s = P (unlift (HD \ s))" \ \this means that for \nil\ and \UU\ the effect is unpredictable\ -definition Next :: "'a temporal \ 'a temporal" (\\(_)\ [80] 80) +definition Next :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Next\\\_)\ [80] 80) where "(\P) s \ (if TL \ s = UU \ TL \ s = nil then P s else P (TL \ s))" definition suffix :: "'a Seq \ 'a Seq \ bool" @@ -31,10 +31,10 @@ definition tsuffix :: "'a Seq \ 'a Seq \ bool" where "tsuffix s2 s \ s2 \ nil \ s2 \ UU \ suffix s2 s" -definition Box :: "'a temporal \ 'a temporal" (\\(_)\ [80] 80) +definition Box :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Box\\\_)\ [80] 80) where "(\P) s \ (\s2. tsuffix s2 s \ P s2)" -definition Diamond :: "'a temporal \ 'a temporal" (\\(_)\ [80] 80) +definition Diamond :: "'a temporal \ 'a temporal" (\(\indent=1 notation=\prefix Diamond\\\_)\ [80] 80) where "\P = (\<^bold>\ (\(\<^bold>\ P)))" definition Leadsto :: "'a temporal \ 'a temporal \ 'a temporal" (infixr \\\ 22) diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/LowerPD.thy Tue Oct 01 23:36:10 2024 +0200 @@ -74,7 +74,7 @@ subsection \Type definition\ -typedef 'a lower_pd (\('(_')\)\) = +typedef 'a lower_pd (\(\notation=\postfix lower_pd\\'(_')\)\) = "{S::'a pd_basis set. lower_le.ideal S}" by (rule lower_le.ex_ideal) @@ -339,10 +339,7 @@ syntax "_lower_bind" :: "[logic, logic, logic] \ logic" - (\(3\\_\_./ _)\ [0, 0, 10] 10) - -syntax_consts - "_lower_bind" == lower_bind + (\(\indent=3 notation=\binder lower_bind\\\\_\_./ _)\ [0, 0, 10] 10) translations "\\x\xs. e" == "CONST lower_bind\xs\(\ x. e)" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Porder.thy --- a/src/HOL/HOLCF/Porder.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Porder.thy Tue Oct 01 23:36:10 2024 +0200 @@ -113,10 +113,10 @@ end syntax (ASCII) - "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(3LUB _:_./ _)\ [0,0, 10] 10) + "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder LUB\\LUB _:_./ _)\ [0,0, 10] 10) syntax - "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(3\_\_./ _)\ [0,0, 10] 10) + "_BLub" :: "[pttrn, 'a set, 'b] \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0,0, 10] 10) syntax_consts "_BLub" \ lub diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Sprod.thy --- a/src/HOL/HOLCF/Sprod.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 01 23:36:10 2024 +0200 @@ -16,7 +16,7 @@ definition "sprod = {p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" -pcpodef ('a, 'b) sprod (\(_ \/ _)\ [21,20] 20) = "sprod :: ('a \ 'b) set" +pcpodef ('a, 'b) sprod (\(\notation=\infix strict product\\_ \/ _)\ [21,20] 20) = "sprod :: ('a \ 'b) set" by (simp_all add: sprod_def) instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Ssum.thy --- a/src/HOL/HOLCF/Ssum.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Ssum.thy Tue Oct 01 23:36:10 2024 +0200 @@ -19,7 +19,7 @@ (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \)}" -pcpodef ('a, 'b) ssum (\(_ \/ _)\ [21, 20] 20) = "ssum :: (tr \ 'a \ 'b) set" +pcpodef ('a, 'b) ssum (\(\notation=\infix strict sum\\_ \/ _)\ [21, 20] 20) = "ssum :: (tr \ 'a \ 'b) set" by (simp_all add: ssum_def) instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Tr.thy --- a/src/HOL/HOLCF/Tr.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Tr.thy Tue Oct 01 23:36:10 2024 +0200 @@ -63,7 +63,7 @@ definition tr_case :: "'a \ 'a \ tr \ 'a" where "tr_case = (\ t e (Def b). if b then t else e)" -abbreviation cifte_syn :: "[tr, 'c, 'c] \ 'c" (\(If (_)/ then (_)/ else (_))\ [0, 0, 60] 60) +abbreviation cifte_syn :: "[tr, 'c, 'c] \ 'c" (\(\notation=\mixfix If expression\\If (_)/ then (_)/ else (_))\ [0, 0, 60] 60) where "If b then e1 else e2 \ tr_case\e1\e2\b" translations diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/Up.thy --- a/src/HOL/HOLCF/Up.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/Up.thy Tue Oct 01 23:36:10 2024 +0200 @@ -14,7 +14,7 @@ subsection \Definition of new type for lifting\ -datatype 'a u (\(_\<^sub>\)\ [1000] 999) = Ibottom | Iup 'a +datatype 'a u (\(\notation=\postfix lifting\\_\<^sub>\)\ [1000] 999) = Ibottom | Iup 'a primrec Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" where diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/UpperPD.thy Tue Oct 01 23:36:10 2024 +0200 @@ -72,7 +72,7 @@ subsection \Type definition\ -typedef 'a upper_pd (\('(_')\)\) = +typedef 'a upper_pd (\(\notation=\postfix upper_pd\\'(_')\)\) = "{S::'a pd_basis set. upper_le.ideal S}" by (rule upper_le.ex_ideal) @@ -332,10 +332,7 @@ syntax "_upper_bind" :: "[logic, logic, logic] \ logic" - (\(3\\_\_./ _)\ [0, 0, 10] 10) - -syntax_consts - "_upper_bind" == upper_bind + (\(\indent=3 notation=\binder upper_bind\\\\_\_./ _)\ [0, 0, 10] 10) translations "\\x\xs. e" == "CONST upper_bind\xs\(\ x. e)" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ex/Letrec.thy --- a/src/HOL/HOLCF/ex/Letrec.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/ex/Letrec.thy Tue Oct 01 23:36:10 2024 +0200 @@ -15,15 +15,12 @@ nonterminal recbinds and recbindt and recbind syntax - "_recbind" :: "[logic, logic] \ recbind" (\(2_ =/ _)\ 10) + "_recbind" :: "[logic, logic] \ recbind" (\(\indent=2 notation=\mixfix Letrec binding\\_ =/ _)\ 10) "" :: "recbind \ recbindt" (\_\) "_recbindt" :: "[recbind, recbindt] \ recbindt" (\_,/ _\) "" :: "recbindt \ recbinds" (\_\) "_recbinds" :: "[recbindt, recbinds] \ recbinds" (\_;/ _\) - "_Letrec" :: "[recbinds, logic] \ logic" (\(Letrec (_)/ in (_))\ 10) - -syntax_consts - "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec + "_Letrec" :: "[recbinds, logic] \ logic" (\(\notation=\mixfix Letrec expression\\Letrec (_)/ in (_))\ 10) translations (recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)" diff -r 2a8afc91ce9c -r 49c04500c5f9 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Oct 01 22:12:11 2024 +0200 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Tue Oct 01 23:36:10 2024 +0200 @@ -103,14 +103,14 @@ nonterminal Case_pat and Case_syn and Cases_syn syntax - "_Case_syntax":: "['a, Cases_syn] => 'b" (\(Case _ of/ _)\ 10) - "_Case1" :: "[Case_pat, 'b] => Case_syn" (\(2_ \/ _)\ 10) + "_Case_syntax":: "['a, Cases_syn] => 'b" (\(\notation=\mixfix Case expression\\Case _ of/ _)\ 10) + "_Case1" :: "[Case_pat, 'b] => Case_syn" (\(\indent=2 notation=\mixfix Case clause\\_ \/ _)\ 10) "" :: "Case_syn => Cases_syn" (\_\) "_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" (\_/ | _\) "_strip_positions" :: "'a => Case_pat" (\_\) syntax (ASCII) - "_Case1" :: "[Case_pat, 'b] => Case_syn" (\(2_ =>/ _)\ 10) + "_Case1" :: "[Case_pat, 'b] => Case_syn" (\(\indent=2 notation=\mixfix Case clause\\_ =>/ _)\ 10) translations "_Case_syntax x ms" == "CONST cases\(ms\x)"