--- a/NEWS Wed Oct 02 18:32:36 2024 +0200
+++ b/NEWS Thu Oct 03 13:01:31 2024 +0200
@@ -9,6 +9,10 @@
*** General ***
+* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
+so its declarations are applied immediately, but also named for later
+re-use.
+
* Inner syntax translations now support formal dependencies via commands
'syntax_types' or 'syntax_consts'. This is essentially an abstract
specification of the effect of 'translations' (or translation functions
@@ -43,6 +47,19 @@
*** HOL ***
+* Various declaration bundles support adhoc modification of notation,
+notably like this:
+
+ unbundle no_list_syntax
+ unbundle no_listcompr_syntax
+ unbundle no_rtrancl_syntax
+ unbundle no_trancl_syntax
+ unbundle no_reflcl_syntax
+
+This is more robust than individual 'no_syntax' / 'no_notation'
+commands, which need to copy mixfix declarations from elsewhere and thus
+break after changes in the library.
+
* Theory "HOL.Wellfounded":
- Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
Minor INCOMPATIBILITIES.
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Thu Oct 03 13:01:31 2024 +0200
@@ -28,8 +28,6 @@
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
- MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/CCL/Set.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Set.thy Thu Oct 03 13:01:31 2024 +0200
@@ -19,8 +19,6 @@
syntax
"_Coll" :: "[idt, o] \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
-syntax_consts
- Collect
translations
"{x. P}" == "CONST Collect(\<lambda>x. P)"
--- a/src/CCL/Term.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Term.thy Thu Oct 03 13:01:31 2024 +0200
@@ -51,7 +51,6 @@
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
translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
@@ -73,7 +72,6 @@
(\<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 letrec2 letrec3
parse_translation \<open>
let
fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
--- a/src/CCL/Type.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/CCL/Type.thy Thu Oct 03 13:01:31 2024 +0200
@@ -14,8 +14,6 @@
syntax
"_Subtype" :: "[idt, 'a set, o] \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Subtype\<close>\<close>{_: _ ./ _})\<close>)
-syntax_consts
- Subtype
translations
"{x: A. B}" == "CONST Subtype(A, \<lambda>x. B)"
--- a/src/Doc/Datatypes/Datatypes.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Oct 03 13:01:31 2024 +0200
@@ -453,8 +453,7 @@
Incidentally, this is how the traditional syntax can be set up:
\<close>
(*<*)
-no_syntax
- "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+unbundle no_list_syntax
(*>*)
syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
--- a/src/Doc/Isar_Ref/Spec.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Oct 03 13:01:31 2024 +0200
@@ -231,7 +231,7 @@
(\secref{sec:locale}).
\<^rail>\<open>
- @@{command bundle} @{syntax name}
+ (@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline>
( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
;
@@{command print_bundles} ('!'?)
@@ -258,6 +258,9 @@
b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
bindings are not recorded in the bundle.
+ \<^descr> \<^theory_text>\<open>open_bundle b\<close> is like \<^theory_text>\<open>bundle b\<close> followed by \<^theory_text>\<open>unbundle b\<close>, so its
+ declarations are applied immediately, but also named for later re-use.
+
\<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
current context; the ``\<open>!\<close>'' option indicates extra verbosity.
--- a/src/Doc/Tutorial/Protocol/Message.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy Thu Oct 03 13:01:31 2024 +0200
@@ -81,8 +81,6 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)")
-syntax_consts
- MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/FOL/IFOL.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/FOL/IFOL.thy Thu Oct 03 13:01:31 2024 +0200
@@ -747,8 +747,6 @@
"" :: \<open>letbind => letbinds\<close> (\<open>_\<close>)
"_binds" :: \<open>[letbind, letbinds] => letbinds\<close> (\<open>_;/ _\<close>)
"_Let" :: \<open>[letbinds, 'a] => 'a\<close> (\<open>(\<open>notation=\<open>mixfix let in\<close>\<close>let (_)/ in (_))\<close> 10)
-syntax_consts
- Let
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
"let x = a in e" == "CONST Let(a, \<lambda>x. e)"
--- a/src/HOL/Analysis/Bochner_Integration.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Thu Oct 03 13:01:31 2024 +0200
@@ -890,7 +890,8 @@
"integral\<^sup>L M f = (if \<exists>x. has_bochner_integral M f x then THE x. has_bochner_integral M f x else 0)"
syntax
- "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real" (\<open>\<integral>((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+ "_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> 'a measure \<Rightarrow> real"
+ (\<open>(\<open>indent=1 notation=\<open>binder integral\<close>\<close>\<integral>(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
syntax_consts
"_lebesgue_integral" == lebesgue_integral
@@ -899,7 +900,8 @@
"\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
syntax
- "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" (\<open>(3LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
+ "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+ (\<open>(\<open>indent=3 notation=\<open>mixfix LINT\<close>\<close>LINT (1_)/|(_)./ _)\<close> [0,110,60] 60)
syntax_consts
"_ascii_lebesgue_integral" == lebesgue_integral
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Thu Oct 03 13:01:31 2024 +0200
@@ -10,7 +10,7 @@
definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
-typedef (overloaded) ('a, 'b) bcontfun (\<open>(_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
+typedef (overloaded) ('a, 'b) bcontfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>C\<close>\<close>_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
"bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
morphisms apply_bcontfun Bcontfun
by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Oct 03 13:01:31 2024 +0200
@@ -116,7 +116,7 @@
subsection \<open>Type of bounded linear functions\<close>
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>L\<close>\<close>_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
"{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
morphisms blinfun_apply Blinfun
by (blast intro: bounded_linear_intros)
--- a/src/HOL/Analysis/Cross3.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy Thu Oct 03 13:01:31 2024 +0200
@@ -21,12 +21,14 @@
end
-bundle cross3_syntax begin
+bundle cross3_syntax
+begin
notation cross3 (infixr \<open>\<times>\<close> 80)
no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
-bundle no_cross3_syntax begin
+bundle no_cross3_syntax
+begin
no_notation cross3 (infixr \<open>\<times>\<close> 80)
notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Oct 03 13:01:31 2024 +0200
@@ -20,20 +20,16 @@
declare vec_lambda_inject [simplified, simp]
-bundle vec_syntax begin
-notation
- vec_nth (infixl \<open>$\<close> 90) and
- vec_lambda (binder \<open>\<chi>\<close> 10)
+open_bundle vec_syntax
+begin
+notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
-bundle no_vec_syntax begin
-no_notation
- vec_nth (infixl \<open>$\<close> 90) and
- vec_lambda (binder \<open>\<chi>\<close> 10)
+bundle no_vec_syntax
+begin
+no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
end
-unbundle vec_syntax
-
text \<open>
Concrete syntax for \<open>('a, 'b) vec\<close>:
\<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Thu Oct 03 13:01:31 2024 +0200
@@ -169,7 +169,8 @@
"Pi\<^sub>M I M \<equiv> PiM I M"
syntax
- "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure" (\<open>(3\<Pi>\<^sub>M _\<in>_./ _)\<close> 10)
+ "_PiM" :: "pttrn \<Rightarrow> 'i set \<Rightarrow> 'a measure \<Rightarrow> ('i => 'a) measure"
+ (\<open>(\<open>indent=3 notation=\<open>binder \<Pi>\<^sub>M\<close>\<close>\<Pi>\<^sub>M _\<in>_./ _)\<close> 10)
syntax_consts
"_PiM" == PiM
translations
--- a/src/HOL/Analysis/Infinite_Set_Sum.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Oct 03 13:01:31 2024 +0200
@@ -96,10 +96,10 @@
syntax (ASCII)
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
"_infsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_\<in>_./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_infsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -107,10 +107,10 @@
syntax (ASCII)
"_uinfsetsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _:_./ _)\<close> [0, 51, 10] 10)
syntax
"_uinfsetsum" :: "pttrn \<Rightarrow> 'b \<Rightarrow> 'b::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_./ _)\<close> [0, 10] 10)
syntax_consts
"_uinfsetsum" \<rightleftharpoons> infsetsum
translations \<comment> \<open>Beware of argument permutation!\<close>
@@ -118,10 +118,10 @@
syntax (ASCII)
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
- (\<open>(3INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSETSUM\<close>\<close>INFSETSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
"_qinfsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a::{banach, second_countable_topology}"
- (\<open>(2\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>a\<close>\<close>\<Sum>\<^sub>a_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qinfsetsum" \<rightleftharpoons> infsetsum
translations
--- a/src/HOL/Analysis/Infinite_Sum.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Thu Oct 03 13:01:31 2024 +0200
@@ -47,27 +47,29 @@
"f abs_summable_on A \<equiv> (\<lambda>x. norm (f x)) summable_on A"
syntax (ASCII)
- "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" (\<open>(3INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+ (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM (_/:_)./ _)\<close> [0, 51, 10] 10)
syntax
- "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add" (\<open>(2\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
+ "_infsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::topological_comm_monoid_add"
+ (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>(_/\<in>_)./ _)\<close> [0, 51, 10] 10)
syntax_consts
"_infsum" \<rightleftharpoons> infsum
translations \<comment> \<open>Beware of argument permutation!\<close>
"\<Sum>\<^sub>\<infinity>i\<in>A. b" \<rightleftharpoons> "CONST infsum (\<lambda>i. b) A"
syntax (ASCII)
- "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3INFSUM _./ _)\<close> [0, 10] 10)
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _./ _)\<close> [0, 10] 10)
syntax
- "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
+ "_univinfsum" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_./ _)\<close> [0, 10] 10)
syntax_consts
"_univinfsum" \<rightleftharpoons> infsum
translations
"\<Sum>\<^sub>\<infinity>x. t" \<rightleftharpoons> "CONST infsum (\<lambda>x. t) (CONST UNIV)"
syntax (ASCII)
- "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder INFSUM\<close>\<close>INFSUM _ |/ _./ _)\<close> [0, 0, 10] 10)
syntax
- "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(2\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qinfsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=2 notation=\<open>binder \<Sum>\<^sub>\<infinity>\<close>\<close>\<Sum>\<^sub>\<infinity>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qinfsum" \<rightleftharpoons> infsum
translations
--- a/src/HOL/Analysis/Inner_Product.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy Thu Oct 03 13:01:31 2024 +0200
@@ -391,9 +391,8 @@
subsection \<open>Gradient derivative\<close>
definition\<^marker>\<open>tag important\<close>
- gderiv ::
- "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
- (\<open>(GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
+ gderiv :: "['a::real_inner \<Rightarrow> real, 'a, 'a] \<Rightarrow> bool"
+ (\<open>(\<open>notation=\<open>mixfix GDERIV\<close>\<close>GDERIV (_)/ (_)/ :> (_))\<close> [1000, 1000, 60] 60)
where
"GDERIV f x :> D \<longleftrightarrow> FDERIV f x :> (\<lambda>h. inner h D)"
@@ -462,11 +461,13 @@
lemmas has_derivative_norm = GDERIV_norm [unfolded gderiv_def]
-bundle inner_syntax begin
+bundle inner_syntax
+begin
notation inner (infix \<open>\<bullet>\<close> 70)
end
-bundle no_inner_syntax begin
+bundle no_inner_syntax
+begin
no_notation inner (infix \<open>\<bullet>\<close> 70)
end
--- a/src/HOL/Analysis/Interval_Integral.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Thu Oct 03 13:01:31 2024 +0200
@@ -146,7 +146,7 @@
syntax
"_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(5LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
+ (\<open>(\<open>indent=5 notation=\<open>binder LINT\<close>\<close>LINT _=_.._|_. _)\<close> [0,60,60,61,100] 60)
syntax_consts
"_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
@@ -160,7 +160,7 @@
syntax
"_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4LBINT _=_.._. _)\<close> [0,60,60,61] 60)
+ (\<open>(\<open>indent=4 notation=\<open>binder LBINT\<close>\<close>LBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
@@ -1049,7 +1049,7 @@
syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(2CLBINT _. _)\<close> [0,60] 60)
+ (\<open>(\<open>indent=2 notation=\<open>binder CLBINT\<close>\<close>CLBINT _. _)\<close> [0,60] 60)
syntax_consts
"_complex_lebesgue_borel_integral" == complex_lebesgue_integral
@@ -1057,7 +1057,7 @@
translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(3CLBINT _:_. _)\<close> [0,60,61] 60)
+ (\<open>(\<open>indent=3 notation=\<open>binder CLBINT\<close>\<close>CLBINT _:_. _)\<close> [0,60,61] 60)
syntax_consts
"_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
@@ -1075,7 +1075,7 @@
syntax
"_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
- (\<open>(4CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
+ (\<open>(\<open>indent=4 notation=\<open>binder CLBINT\<close>\<close>CLBINT _=_.._. _)\<close> [0,60,60,61] 60)
syntax_consts
"_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
--- a/src/HOL/Analysis/Lipschitz.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy Thu Oct 03 13:01:31 2024 +0200
@@ -12,15 +12,16 @@
definition\<^marker>\<open>tag important\<close> lipschitz_on
where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
-bundle lipschitz_syntax begin
+open_bundle lipschitz_syntax
+begin
notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
-bundle no_lipschitz_syntax begin
+
+bundle no_lipschitz_syntax
+begin
no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
end
-unbundle lipschitz_syntax
-
lemma lipschitz_onI: "L-lipschitz_on X f"
if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L"
using that by (auto simp: lipschitz_on_def)
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Thu Oct 03 13:01:31 2024 +0200
@@ -820,7 +820,7 @@
"integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
syntax
- "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>\<integral>\<^sup>+((2 _./ _)/ \<partial>_)\<close> [60,61] 110)
+ "_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" (\<open>(\<open>indent=2 notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+(2 _./ _)/ \<partial>_)\<close> [60,61] 110)
syntax_consts
"_nn_integral" == nn_integral
--- a/src/HOL/Analysis/Set_Integral.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Thu Oct 03 13:01:31 2024 +0200
@@ -24,7 +24,7 @@
syntax
"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
+ (\<open>(\<open>indent=4 notation=\<open>binder LINT\<close>\<close>LINT (_):(_)/|(_)./ _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_set_lebesgue_integral" == set_lebesgue_integral
@@ -43,11 +43,11 @@
syntax
"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
- (\<open>(2LBINT _./ _)\<close> [0,10] 10)
+ (\<open>(\<open>indent=2 notation=\<open>binder LBINT\<close>\<close>LBINT _./ _)\<close> [0,10] 10)
syntax
"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
- (\<open>(3LBINT _:_./ _)\<close> [0,0,10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder LBINT\<close>\<close>LBINT _:_./ _)\<close> [0,0,10] 10)
section \<open>Basic properties\<close>
@@ -587,7 +587,7 @@
syntax
"_ascii_complex_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(3CLINT _|_. _)\<close> [0,0,10] 10)
+ (\<open>(\<open>indent=3 notation=\<open>binder CLINT\<close>\<close>CLINT _|_. _)\<close> [0,0,10] 10)
syntax_consts
"_ascii_complex_lebesgue_integral" == complex_lebesgue_integral
@@ -624,7 +624,7 @@
syntax
"_ascii_complex_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
- (\<open>(4CLINT _:_|_. _)\<close> [0,0,0,10] 10)
+ (\<open>(\<open>indent=4 notation=\<open>binder CLINT\<close>\<close>CLINT _:_|_. _)\<close> [0,0,0,10] 10)
syntax_consts
"_ascii_complex_set_lebesgue_integral" == complex_set_lebesgue_integral
@@ -647,10 +647,10 @@
syntax
"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
-(\<open>(\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
+(\<open>(\<open>notation=\<open>binder integral\<close>\<close>\<integral>((_)\<in>(_)./ _)/\<partial>_)\<close> [0,0,0,110] 10)
syntax_consts
"_set_nn_integral" == set_nn_integral and
--- a/src/HOL/Analysis/Sparse_In.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy Thu Oct 03 13:01:31 2024 +0200
@@ -165,14 +165,14 @@
"cosparse A = Abs_filter (\<lambda>P. {x. \<not>P x} sparse_in A)"
syntax
- "_eventually_cosparse" :: "pttrn => 'a set => bool => bool" (\<open>(3\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
+ "_eventually_cosparse" :: "pttrn => 'a set => bool => bool" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_\<in>_./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_eventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
syntax
- "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(3\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
+ "_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" (\<open>(\<open>indent=3 notation=\<open>binder \<forall>\<approx>\<close>\<close>\<forall>\<^sub>\<approx>_ | (_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
"_qeventually_cosparse" == eventually
translations
--- a/src/HOL/Auth/Message.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Auth/Message.thy Thu Oct 03 13:01:31 2024 +0200
@@ -51,8 +51,6 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
- MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/HOL/Code_Evaluation.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Code_Evaluation.thy Thu Oct 03 13:01:31 2024 +0200
@@ -54,10 +54,7 @@
bundle term_syntax
begin
-
-notation App (infixl \<open><\<cdot>>\<close> 70)
- and valapp (infixl \<open>{\<cdot>}\<close> 70)
-
+notation App (infixl \<open><\<cdot>>\<close> 70) and valapp (infixl \<open>{\<cdot>}\<close> 70)
end
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy Thu Oct 03 13:01:31 2024 +0200
@@ -24,9 +24,7 @@
no_notation lazy_llist (\<open>_\<close>)
syntax
- "_llist" :: "args => 'a list" (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>)
-syntax_consts
- lazy_llist
+ "_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>[_\<^bold>])\<close>)
translations
"\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
"\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
--- a/src/HOL/Combinatorics/Perm.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy Thu Oct 03 13:01:31 2024 +0200
@@ -792,20 +792,18 @@
subsection \<open>Syntax\<close>
-bundle no_permutation_syntax
+open_bundle no_permutation_syntax
begin
- no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
- no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
- no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
+no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
end
bundle permutation_syntax
begin
- notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
- notation cycle (\<open>\<langle>_\<rangle>\<close>)
- notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+notation cycle (\<open>\<langle>_\<rangle>\<close>)
+notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
end
-unbundle no_permutation_syntax
-
end
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Oct 03 13:01:31 2024 +0200
@@ -25,7 +25,7 @@
setup_lifting type_definition_fls
-unbundle fps_notation
+unbundle fps_syntax
notation fls_nth (infixl \<open>$$\<close> 75)
lemmas fls_eqI = iffD1[OF fls_nth_inject, OF iffD2, OF fun_eq_iff, OF allI]
@@ -4603,7 +4603,7 @@
no_notation fls_nth (infixl \<open>$$\<close> 75)
-bundle fls_notation
+bundle fps_syntax
begin
notation fls_nth (infixl \<open>$$\<close> 75)
end
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Oct 03 13:01:31 2024 +0200
@@ -6193,7 +6193,7 @@
(* TODO: Figure out better notation for this thing *)
no_notation fps_nth (infixl \<open>$\<close> 75)
-bundle fps_notation
+bundle fps_syntax
begin
notation fps_nth (infixl \<open>$\<close> 75)
end
--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Thu Oct 03 13:01:31 2024 +0200
@@ -349,9 +349,7 @@
subsection \<open>List-style syntax for polynomials\<close>
syntax
- "_poly" :: "args \<Rightarrow> 'a poly" (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
-syntax_consts
- pCons
+ "_poly" :: "args \<Rightarrow> 'a poly" (\<open>(\<open>indent=2 notation=\<open>mixfix polynomial enumeration\<close>\<close>[:_:])\<close>)
translations
"[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
"[:x:]" \<rightleftharpoons> "CONST pCons x 0"
--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy Thu Oct 03 13:01:31 2024 +0200
@@ -9,7 +9,7 @@
begin
context
- includes fps_notation
+ includes fps_syntax
begin
definition fps_of_poly where
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Oct 03 13:01:31 2024 +0200
@@ -1143,7 +1143,8 @@
section "Avoid pollution of name space"
-bundle floatarith_notation begin
+bundle floatarith_syntax
+begin
notation Add (\<open>Add\<close>)
notation Minus (\<open>Minus\<close>)
@@ -1166,7 +1167,8 @@
end
-bundle no_floatarith_notation begin
+bundle no_floatarith_syntax
+begin
no_notation Add (\<open>Add\<close>)
no_notation Minus (\<open>Minus\<close>)
--- a/src/HOL/Fun.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Fun.thy Thu Oct 03 13:01:31 2024 +0200
@@ -846,9 +846,6 @@
"_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" (\<open>_/'((2_)')\<close> [1000, 0] 900)
-syntax_consts
- fun_upd
-
translations
"_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
"f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
--- a/src/HOL/HOL.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOL.thy Thu Oct 03 13:01:31 2024 +0200
@@ -191,11 +191,11 @@
nonterminal case_syn and cases_syn
syntax
"_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b" (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
- "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
+ "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
"" :: "case_syn \<Rightarrow> cases_syn" (\<open>_\<close>)
"_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn" (\<open>_/ | _\<close>)
syntax (ASCII)
- "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
+ "_case1" :: "['a, 'b] \<Rightarrow> case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ =>/ _)\<close> 10)
notation (ASCII)
All (binder \<open>ALL \<close> 10) and
--- a/src/HOL/HOLCF/Cfun.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Thu Oct 03 13:01:31 2024 +0200
@@ -16,17 +16,17 @@
definition "cfun = {f::'a \<Rightarrow> 'b. cont f}"
-cpodef ('a, 'b) cfun (\<open>(_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
+cpodef ('a, 'b) cfun (\<open>(\<open>notation=\<open>infix \<rightarrow>\<close>\<close>_ \<rightarrow>/ _)\<close> [1, 0] 0) = "cfun :: ('a \<Rightarrow> 'b) set"
by (auto simp: cfun_def intro: cont_const adm_cont)
type_notation (ASCII)
cfun (infixr \<open>->\<close> 0)
notation (ASCII)
- Rep_cfun (\<open>(_$/_)\<close> [999,1000] 999)
+ Rep_cfun (\<open>(\<open>notation=\<open>infix $\<close>\<close>_$/_)\<close> [999,1000] 999)
notation
- Rep_cfun (\<open>(_\<cdot>/_)\<close> [999,1000] 999)
+ Rep_cfun (\<open>(\<open>notation=\<open>infix \<cdot>\<close>\<close>_\<cdot>/_)\<close> [999,1000] 999)
subsection \<open>Syntax for continuous lambda abstraction\<close>
@@ -47,10 +47,10 @@
text \<open>Syntax for nested abstractions\<close>
syntax (ASCII)
- "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(3LAM _./ _)\<close> [1000, 10] 10)
+ "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(\<open>indent=3 notation=\<open>binder LAM\<close>\<close>LAM _./ _)\<close> [1000, 10] 10)
syntax
- "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(3\<Lambda> _./ _)\<close> [1000, 10] 10)
+ "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" (\<open>(\<open>indent=3 notation=\<open>binder \<Lambda>\<close>\<close>\<Lambda> _./ _)\<close> [1000, 10] 10)
syntax_consts
"_Lambda" \<rightleftharpoons> Abs_cfun
--- a/src/HOL/HOLCF/ConvexPD.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy Thu Oct 03 13:01:31 2024 +0200
@@ -119,7 +119,7 @@
subsection \<open>Type definition\<close>
-typedef 'a convex_pd (\<open>('(_')\<natural>)\<close>) =
+typedef 'a convex_pd (\<open>(\<open>notation=\<open>postfix convex_pd\<close>\<close>'(_')\<natural>)\<close>) =
"{S::'a pd_basis set. convex_le.ideal S}"
by (rule convex_le.ex_ideal)
@@ -178,13 +178,8 @@
(infixl \<open>\<union>\<natural>\<close> 65) where
"xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
-nonterminal convex_pd_args
syntax
- "" :: "logic \<Rightarrow> convex_pd_args" (\<open>_\<close>)
- "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args" (\<open>_,/ _\<close>)
- "_convex_pd" :: "convex_pd_args \<Rightarrow> logic" (\<open>{_}\<natural>\<close>)
-syntax_consts
- "_convex_pd_args" "_convex_pd" == convex_add
+ "_convex_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix convex_pd enumeration\<close>\<close>{_}\<natural>)\<close>)
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
"{x}\<natural>" == "CONST convex_unit\<cdot>x"
@@ -350,10 +345,7 @@
syntax
"_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
- (\<open>(3\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
- "_convex_bind" == convex_bind
+ (\<open>(\<open>indent=3 notation=\<open>binder convex_bind\<close>\<close>\<Union>\<natural>_\<in>_./ _)\<close> [0, 0, 10] 10)
translations
"\<Union>\<natural>x\<in>xs. e" == "CONST convex_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Thu Oct 03 13:01:31 2024 +0200
@@ -29,16 +29,16 @@
"<> == \<bottom>"
abbreviation
- fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(_\<leadsto>_)\<close> [66,65] 65) where
+ fscons' :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_\<leadsto>_)\<close> [66,65] 65) where
"a\<leadsto>s == fscons a\<cdot>s"
abbreviation
- fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+ fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
"A\<copyright>s == fsfilter A\<cdot>s"
notation (ASCII)
- fscons' (\<open>(_~>_)\<close> [66,65] 65) and
- fsfilter' (\<open>(_'(C')_)\<close> [64,63] 63)
+ fscons' (\<open>(\<open>notation=\<open>infix ~>\<close>\<close>_~>_)\<close> [66,65] 65) and
+ fsfilter' (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Thu Oct 03 13:01:31 2024 +0200
@@ -44,11 +44,11 @@
"<> == \<bottom>"
abbreviation
- fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(_\<copyright>_)\<close> [64,63] 63) where
+ fsfilter' :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" (\<open>(\<open>notation=\<open>infix \<copyright>\<close>\<close>_\<copyright>_)\<close> [64,63] 63) where
"A\<copyright>s == fsfilter A\<cdot>s"
notation (ASCII)
- fsfilter' (\<open>(_'(C')_)\<close> [64,63] 63)
+ fsfilter' (\<open>(\<open>notation=\<open>infix (C)\<close>\<close>_'(C')_)\<close> [64,63] 63)
lemma ft_fsingleton[simp]: "ft\<cdot>(<a>) = Def a"
--- a/src/HOL/HOLCF/IOA/Sequence.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy Thu Oct 03 13:01:31 2024 +0200
@@ -63,17 +63,15 @@
UU \<Rightarrow> UU
| Def y \<Rightarrow> (if P y then x ## (h \<cdot> xs) else h \<cdot> xs))))"
-abbreviation Consq_syn (\<open>(_/\<leadsto>_)\<close> [66, 65] 65)
+abbreviation Consq_syn (\<open>(\<open>notation=\<open>infix \<leadsto>\<close>\<close>_/\<leadsto>_)\<close> [66, 65] 65)
where "a \<leadsto> s \<equiv> Consq a \<cdot> s"
subsection \<open>List enumeration\<close>
syntax
- "_totlist" :: "args \<Rightarrow> 'a Seq" (\<open>[(\<open>notation=\<open>mixfix total list enumeration\<close>\<close>_)!]\<close>)
- "_partlist" :: "args \<Rightarrow> 'a Seq" (\<open>[(\<open>notation=\<open>mixfix partial list enumeration\<close>\<close>_)?]\<close>)
-syntax_consts
- Consq
+ "_totlist" :: "args \<Rightarrow> 'a Seq" (\<open>(\<open>indent=1 notation=\<open>mixfix total list enumeration\<close>\<close>[_!])\<close>)
+ "_partlist" :: "args \<Rightarrow> 'a Seq" (\<open>(\<open>indent=1 notation=\<open>mixfix partial list enumeration\<close>\<close>[_?])\<close>)
translations
"[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
"[x!]" \<rightleftharpoons> "x\<leadsto>nil"
--- a/src/HOL/HOLCF/IOA/TL.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/IOA/TL.thy Thu Oct 03 13:01:31 2024 +0200
@@ -22,7 +22,7 @@
where "Init P s = P (unlift (HD \<cdot> s))"
\<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
-definition Next :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<circle>(_)\<close> [80] 80)
+definition Next :: "'a temporal \<Rightarrow> 'a temporal" (\<open>(\<open>indent=1 notation=\<open>prefix Next\<close>\<close>\<circle>_)\<close> [80] 80)
where "(\<circle>P) s \<longleftrightarrow> (if TL \<cdot> s = UU \<or> TL \<cdot> s = nil then P s else P (TL \<cdot> s))"
definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
@@ -31,10 +31,10 @@
definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s"
-definition Box :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<box>(_)\<close> [80] 80)
+definition Box :: "'a temporal \<Rightarrow> 'a temporal" (\<open>(\<open>indent=1 notation=\<open>prefix Box\<close>\<close>\<box>_)\<close> [80] 80)
where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)"
-definition Diamond :: "'a temporal \<Rightarrow> 'a temporal" (\<open>\<diamond>(_)\<close> [80] 80)
+definition Diamond :: "'a temporal \<Rightarrow> 'a temporal" (\<open>(\<open>indent=1 notation=\<open>prefix Diamond\<close>\<close>\<diamond>_)\<close> [80] 80)
where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))"
definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal" (infixr \<open>\<leadsto>\<close> 22)
--- a/src/HOL/HOLCF/LowerPD.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/LowerPD.thy Thu Oct 03 13:01:31 2024 +0200
@@ -74,7 +74,7 @@
subsection \<open>Type definition\<close>
-typedef 'a lower_pd (\<open>('(_')\<flat>)\<close>) =
+typedef 'a lower_pd (\<open>(\<open>notation=\<open>postfix lower_pd\<close>\<close>'(_')\<flat>)\<close>) =
"{S::'a pd_basis set. lower_le.ideal S}"
by (rule lower_le.ex_ideal)
@@ -133,13 +133,8 @@
(infixl \<open>\<union>\<flat>\<close> 65) where
"xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
-nonterminal lower_pd_args
syntax
- "" :: "logic \<Rightarrow> lower_pd_args" (\<open>_\<close>)
- "_lower_pd_args" :: "logic \<Rightarrow> lower_pd_args \<Rightarrow> lower_pd_args" (\<open>_,/ _\<close>)
- "_lower_pd" :: "lower_pd_args \<Rightarrow> logic" (\<open>{_}\<flat>\<close>)
-syntax_consts
- "_lower_pd_args" "_lower_pd" == lower_add
+ "_lower_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix lower_pd enumeration\<close>\<close>{_}\<flat>)\<close>)
translations
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
"{x}\<flat>" == "CONST lower_unit\<cdot>x"
@@ -344,10 +339,7 @@
syntax
"_lower_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
- (\<open>(3\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
- "_lower_bind" == lower_bind
+ (\<open>(\<open>indent=3 notation=\<open>binder lower_bind\<close>\<close>\<Union>\<flat>_\<in>_./ _)\<close> [0, 0, 10] 10)
translations
"\<Union>\<flat>x\<in>xs. e" == "CONST lower_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/Pcpo.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Pcpo.thy Thu Oct 03 13:01:31 2024 +0200
@@ -151,10 +151,7 @@
end
text \<open>Old "UU" syntax:\<close>
-
-syntax UU :: logic
-syntax_consts UU \<rightleftharpoons> bottom
-translations "UU" \<rightharpoonup> "CONST bottom"
+abbreviation (input) "UU \<equiv> bottom"
text \<open>Simproc to rewrite \<^term>\<open>\<bottom> = x\<close> to \<^term>\<open>x = \<bottom>\<close>.\<close>
setup \<open>Reorient_Proc.add (fn \<^Const_>\<open>bottom _\<close> => true | _ => false)\<close>
--- a/src/HOL/HOLCF/Porder.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Porder.thy Thu Oct 03 13:01:31 2024 +0200
@@ -113,10 +113,10 @@
end
syntax (ASCII)
- "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3LUB _:_./ _)\<close> [0,0, 10] 10)
+ "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder LUB\<close>\<close>LUB _:_./ _)\<close> [0,0, 10] 10)
syntax
- "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(3\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
+ "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0,0, 10] 10)
syntax_consts
"_BLub" \<rightleftharpoons> lub
--- a/src/HOL/HOLCF/Sprod.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy Thu Oct 03 13:01:31 2024 +0200
@@ -16,7 +16,7 @@
definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
-pcpodef ('a, 'b) sprod (\<open>(_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod (\<open>(\<open>notation=\<open>infix strict product\<close>\<close>_ \<otimes>/ _)\<close> [21,20] 20) = "sprod :: ('a \<times> 'b) set"
by (simp_all add: sprod_def)
instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
@@ -42,8 +42,6 @@
syntax
"_stuple" :: "[logic, args] \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>)
-syntax_consts
- spair
translations
"(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
"(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/HOLCF/Ssum.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Ssum.thy Thu Oct 03 13:01:31 2024 +0200
@@ -19,7 +19,7 @@
(fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
(fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
-pcpodef ('a, 'b) ssum (\<open>(_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum (\<open>(\<open>notation=\<open>infix strict sum\<close>\<close>_ \<oplus>/ _)\<close> [21, 20] 20) = "ssum :: (tr \<times> 'a \<times> 'b) set"
by (simp_all add: ssum_def)
instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
--- a/src/HOL/HOLCF/Tr.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Tr.thy Thu Oct 03 13:01:31 2024 +0200
@@ -63,7 +63,7 @@
definition tr_case :: "'a \<rightarrow> 'a \<rightarrow> tr \<rightarrow> 'a"
where "tr_case = (\<Lambda> t e (Def b). if b then t else e)"
-abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" (\<open>(If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
+abbreviation cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" (\<open>(\<open>notation=\<open>mixfix If expression\<close>\<close>If (_)/ then (_)/ else (_))\<close> [0, 0, 60] 60)
where "If b then e1 else e2 \<equiv> tr_case\<cdot>e1\<cdot>e2\<cdot>b"
translations
--- a/src/HOL/HOLCF/Up.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/Up.thy Thu Oct 03 13:01:31 2024 +0200
@@ -14,7 +14,7 @@
subsection \<open>Definition of new type for lifting\<close>
-datatype 'a u (\<open>(_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
+datatype 'a u (\<open>(\<open>notation=\<open>postfix lifting\<close>\<close>_\<^sub>\<bottom>)\<close> [1000] 999) = Ibottom | Iup 'a
primrec Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
where
--- a/src/HOL/HOLCF/UpperPD.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/UpperPD.thy Thu Oct 03 13:01:31 2024 +0200
@@ -72,7 +72,7 @@
subsection \<open>Type definition\<close>
-typedef 'a upper_pd (\<open>('(_')\<sharp>)\<close>) =
+typedef 'a upper_pd (\<open>(\<open>notation=\<open>postfix upper_pd\<close>\<close>'(_')\<sharp>)\<close>) =
"{S::'a pd_basis set. upper_le.ideal S}"
by (rule upper_le.ex_ideal)
@@ -131,13 +131,8 @@
(infixl \<open>\<union>\<sharp>\<close> 65) where
"xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
-nonterminal upper_pd_args
syntax
- "" :: "logic \<Rightarrow> upper_pd_args" (\<open>_\<close>)
- "_upper_pd_args" :: "logic \<Rightarrow> upper_pd_args \<Rightarrow> upper_pd_args" (\<open>_,/ _\<close>)
- "_upper_pd" :: "upper_pd_args \<Rightarrow> logic" (\<open>{_}\<sharp>\<close>)
-syntax_consts
- "_upper_pd_args" "_upper_pd" == upper_add
+ "_upper_pd" :: "args \<Rightarrow> logic" (\<open>(\<open>indent=1 notation=\<open>mixfix upper_pd enumeration\<close>\<close>{_}\<sharp>)\<close>)
translations
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
"{x}\<sharp>" == "CONST upper_unit\<cdot>x"
@@ -337,10 +332,7 @@
syntax
"_upper_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
- (\<open>(3\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
-
-syntax_consts
- "_upper_bind" == upper_bind
+ (\<open>(\<open>indent=3 notation=\<open>binder upper_bind\<close>\<close>\<Union>\<sharp>_\<in>_./ _)\<close> [0, 0, 10] 10)
translations
"\<Union>\<sharp>x\<in>xs. e" == "CONST upper_bind\<cdot>xs\<cdot>(\<Lambda> x. e)"
--- a/src/HOL/HOLCF/ex/Letrec.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ex/Letrec.thy Thu Oct 03 13:01:31 2024 +0200
@@ -15,15 +15,12 @@
nonterminal recbinds and recbindt and recbind
syntax
- "_recbind" :: "[logic, logic] \<Rightarrow> recbind" (\<open>(2_ =/ _)\<close> 10)
+ "_recbind" :: "[logic, logic] \<Rightarrow> recbind" (\<open>(\<open>indent=2 notation=\<open>mixfix Letrec binding\<close>\<close>_ =/ _)\<close> 10)
"" :: "recbind \<Rightarrow> recbindt" (\<open>_\<close>)
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" (\<open>_,/ _\<close>)
"" :: "recbindt \<Rightarrow> recbinds" (\<open>_\<close>)
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" (\<open>_;/ _\<close>)
- "_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" (\<open>(Letrec (_)/ in (_))\<close> 10)
-
-syntax_consts
- "_recbind" "_recbinds" "_recbindt" "_Letrec" == CLetrec
+ "_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" (\<open>(\<open>notation=\<open>mixfix Letrec expression\<close>\<close>Letrec (_)/ in (_))\<close> 10)
translations
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Thu Oct 03 13:01:31 2024 +0200
@@ -103,14 +103,14 @@
nonterminal Case_pat and Case_syn and Cases_syn
syntax
- "_Case_syntax":: "['a, Cases_syn] => 'b" (\<open>(Case _ of/ _)\<close> 10)
- "_Case1" :: "[Case_pat, 'b] => Case_syn" (\<open>(2_ \<Rightarrow>/ _)\<close> 10)
+ "_Case_syntax":: "['a, Cases_syn] => 'b" (\<open>(\<open>notation=\<open>mixfix Case expression\<close>\<close>Case _ of/ _)\<close> 10)
+ "_Case1" :: "[Case_pat, 'b] => Case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
"" :: "Case_syn => Cases_syn" (\<open>_\<close>)
"_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" (\<open>_/ | _\<close>)
"_strip_positions" :: "'a => Case_pat" (\<open>_\<close>)
syntax (ASCII)
- "_Case1" :: "[Case_pat, 'b] => Case_syn" (\<open>(2_ =>/ _)\<close> 10)
+ "_Case1" :: "[Case_pat, 'b] => Case_syn" (\<open>(\<open>indent=2 notation=\<open>mixfix Case clause\<close>\<close>_ =>/ _)\<close> 10)
translations
"_Case_syntax x ms" == "CONST cases\<cdot>(ms\<cdot>x)"
--- a/src/HOL/Library/FSet.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/FSet.thy Thu Oct 03 13:01:31 2024 +0200
@@ -165,9 +165,7 @@
by simp
syntax
- "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
- finsert
+ "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
translations
"{|x, xs|}" == "CONST finsert x {|xs|}"
"{|x|}" == "CONST finsert x {||}"
@@ -194,26 +192,49 @@
end
syntax (input)
- "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
- "_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite !\<close>\<close>! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite ?\<close>\<close>? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite ?!\<close>\<close>?! (_/:_)./ _)\<close> [0, 0, 10] 10)
syntax
- "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
- "_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(3\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBnex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<nexists>\<close>\<close>\<nexists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+ "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>!\<close>\<close>\<exists>!(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
syntax_consts
- "_fBall" \<rightleftharpoons> FSet.Ball and
- "_fBex" \<rightleftharpoons> FSet.Bex
+ "_fBall" "_fBnex" \<rightleftharpoons> fBall and
+ "_fBex" \<rightleftharpoons> fBex and
+ "_fBex1" \<rightleftharpoons> Ex1
translations
"\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
"\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
+ "\<nexists>x|\<in>|A. P" \<rightleftharpoons> "CONST fBall A (\<lambda>x. \<not> P)"
+ "\<exists>!x|\<in>|A. P" \<rightharpoonup> "\<exists>!x. x |\<in>| A \<and> P"
print_translation \<open>
[Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBall\<close> \<^syntax_const>\<open>_fBall\<close>,
Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBex\<close> \<^syntax_const>\<open>_fBex\<close>]
\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+syntax
+ "_setlessfAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subset>|_./ _)\<close> [0, 0, 10] 10)
+ "_setlessfEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subset>|_./ _)\<close> [0, 0, 10] 10)
+ "_setlefAll" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+ "_setlefEx" :: "[idt, 'a, bool] \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+
+syntax_consts
+ "_setlessfAll" "_setlefAll" \<rightleftharpoons> All and
+ "_setlessfEx" "_setlefEx" \<rightleftharpoons> Ex
+
+translations
+ "\<forall>A|\<subset>|B. P" \<rightharpoonup> "\<forall>A. A |\<subset>| B \<longrightarrow> P"
+ "\<exists>A|\<subset>|B. P" \<rightharpoonup> "\<exists>A. A |\<subset>| B \<and> P"
+ "\<forall>A|\<subseteq>|B. P" \<rightharpoonup> "\<forall>A. A |\<subseteq>| B \<longrightarrow> P"
+ "\<exists>A|\<subseteq>|B. P" \<rightharpoonup> "\<exists>A. A |\<subseteq>| B \<and> P"
+
+
context includes lifting_syntax
begin
--- a/src/HOL/Library/Landau_Symbols.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Thu Oct 03 13:01:31 2024 +0200
@@ -1741,7 +1741,7 @@
abbreviation (input) asymp_equiv_at_top where
"asymp_equiv_at_top f g \<equiv> f \<sim>[at_top] g"
-bundle asymp_equiv_notation
+bundle asymp_equiv_syntax
begin
notation asymp_equiv_at_top (infix \<open>\<sim>\<close> 50)
end
--- a/src/HOL/Library/Multiset.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Oct 03 13:01:31 2024 +0200
@@ -92,9 +92,7 @@
by (rule add_mset_in_multiset)
syntax
- "_multiset" :: "args \<Rightarrow> 'a multiset" (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
-syntax_consts
- add_mset
+ "_multiset" :: "args \<Rightarrow> 'a multiset" (\<open>(\<open>indent=2 notation=\<open>mixfix multiset enumeration\<close>\<close>{#_#})\<close>)
translations
"{#x, xs#}" == "CONST add_mset x {#xs#}"
"{#x#}" == "CONST add_mset x {#}"
--- a/src/HOL/List.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/List.thy Thu Oct 03 13:01:31 2024 +0200
@@ -46,12 +46,16 @@
text \<open>List enumeration\<close>
syntax
- "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
- Cons
+ "_list" :: "args \<Rightarrow> 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
translations
- "[x, xs]" == "x#[xs]"
- "[x]" == "x#[]"
+ "[x, xs]" \<rightleftharpoons> "x#[xs]"
+ "[x]" \<rightleftharpoons> "x#[]"
+
+bundle no_list_syntax
+begin
+no_syntax
+ "_list" :: "args \<Rightarrow> 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
+end
subsection \<open>Basic list processing functions\<close>
@@ -137,9 +141,6 @@
"_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" (\<open>_,/ _\<close>)
"_LUpdate" :: "['a, lupdbinds] => 'a" (\<open>_/[(_)]\<close> [1000,0] 900)
-syntax_consts
- list_update
-
translations
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
"xs[i:=x]" == "CONST list_update xs i x"
@@ -456,6 +457,13 @@
syntax (ASCII)
"_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" (\<open>_ <- _\<close>)
+bundle no_listcompr_syntax
+begin
+no_syntax
+ "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list" (\<open>[_ . __\<close>)
+ "_lc_end" :: "lc_quals" (\<open>]\<close>)
+end
+
parse_translation \<open>
let
val NilC = Syntax.const \<^const_syntax>\<open>Nil\<close>;
--- a/src/HOL/Metis_Examples/Message.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy Thu Oct 03 13:01:31 2024 +0200
@@ -50,8 +50,6 @@
text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
- MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/HOL/Product_Type.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Product_Type.thy Thu Oct 03 13:01:31 2024 +0200
@@ -294,7 +294,6 @@
"_patterns" :: "pttrn \<Rightarrow> patterns \<Rightarrow> patterns" (\<open>_,/ _\<close>)
"_unit" :: pttrn (\<open>'(')\<close>)
syntax_consts
- Pair and
"_pattern" "_patterns" \<rightleftharpoons> case_prod and
"_unit" \<rightleftharpoons> case_unit
translations
@@ -804,10 +803,8 @@
bundle state_combinator_syntax
begin
-
notation fcomp (infixl \<open>\<circ>>\<close> 60)
notation scomp (infixl \<open>\<circ>\<rightarrow>\<close> 60)
-
end
context
@@ -1000,15 +997,19 @@
definition Sigma :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<times> 'b) set"
where "Sigma A B \<equiv> \<Union>x\<in>A. \<Union>y\<in>B x. {Pair x y}"
-abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr \<open>\<times>\<close> 80)
+context
+begin
+qualified abbreviation Times :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" (infixr \<open>\<times>\<close> 80)
where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
+end
-hide_const (open) Times
-
-bundle no_Set_Product_syntax begin
+bundle no_Set_Product_syntax
+begin
no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
-bundle Set_Product_syntax begin
+
+bundle Set_Product_syntax
+begin
notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
end
--- a/src/HOL/Prolog/Test.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Prolog/Test.thy Thu Oct 03 13:01:31 2024 +0200
@@ -19,9 +19,7 @@
text \<open>List enumeration\<close>
syntax
- "_list" :: "args => 'a list" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
- Cons
+ "_list" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Oct 03 13:01:31 2024 +0200
@@ -96,9 +96,7 @@
end
syntax
- "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
- fcons
+ "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
translations
"{|x, xs|}" == "CONST fcons x {|xs|}"
"{|x|}" == "CONST fcons x {||}"
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy Thu Oct 03 13:01:31 2024 +0200
@@ -289,9 +289,7 @@
is "Cons" by auto
syntax
- "_fset" :: "args => 'a fset" (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
-syntax_consts
- insert_fset
+ "_fset" :: "args => 'a fset" (\<open>(\<open>indent=2 notation=\<open>mixfix finite set enumeration\<close>\<close>{|_|})\<close>)
translations
"{|x, xs|}" == "CONST insert_fset x {|xs|}"
"{|x|}" == "CONST insert_fset x {||}"
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Thu Oct 03 13:01:31 2024 +0200
@@ -1716,7 +1716,7 @@
shows "f \<sim>[at_top] eval_monom (dominant_term_ms_aux xs) basis" (is ?thesis1)
and "eventually (\<lambda>x. sgn (f x) = sgn (fst (dominant_term_ms_aux xs))) at_top" (is ?thesis2)
proof -
- include asymp_equiv_notation
+ include asymp_equiv_syntax
from xs(2,1) obtain xs' C b e basis' where xs':
"trimmed C" "xs = MSLCons (C, e) xs'" "basis = b # basis'"
"is_expansion_aux xs' (\<lambda>x. f x - eval C x * b x powr e) (b # basis')"
--- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy Thu Oct 03 13:01:31 2024 +0200
@@ -4,7 +4,7 @@
begin
context
- includes asymp_equiv_notation
+ includes asymp_equiv_syntax
begin
subsection \<open>Dominik Gruntz's examples\<close>
--- a/src/HOL/SET_Protocol/Message_SET.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Oct 03 13:01:31 2024 +0200
@@ -70,8 +70,6 @@
(*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
syntax
"_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
-syntax_consts
- MPair
translations
"\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
"\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
--- a/src/HOL/Set.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Set.thy Thu Oct 03 13:01:31 2024 +0200
@@ -39,18 +39,14 @@
text \<open>Set comprehensions\<close>
syntax
- "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
-syntax_consts
- "_Coll" \<rightleftharpoons> Collect
+ "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_./ _})\<close>)
translations
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
syntax (ASCII)
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/: _)./ _})\<close>)
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/: _)./ _})\<close>)
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/ \<in> _)./ _})\<close>)
-syntax_consts
- "_Collect" \<rightleftharpoons> Collect
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/ \<in> _)./ _})\<close>)
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
@@ -144,9 +140,7 @@
where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
syntax
- "_Finset" :: "args \<Rightarrow> 'a set" (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
-syntax_consts
- insert
+ "_Finset" :: "args \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
translations
"{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
"{x}" \<rightleftharpoons> "CONST insert x {}"
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Thu Oct 03 13:01:31 2024 +0200
@@ -245,7 +245,7 @@
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
- |> Bundle.bundle ((binding, [restore_lifting_att])) []
+ |> Bundle.bundle {open_bundle = false} ((binding, [restore_lifting_att])) []
|> pair binding
end
--- a/src/HOL/Transfer.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Transfer.thy Thu Oct 03 13:01:31 2024 +0200
@@ -13,8 +13,8 @@
bundle lifting_syntax
begin
- notation rel_fun (infixr \<open>===>\<close> 55)
- notation map_fun (infixr \<open>--->\<close> 55)
+notation rel_fun (infixr \<open>===>\<close> 55)
+notation map_fun (infixr \<open>--->\<close> 55)
end
context includes lifting_syntax
--- a/src/HOL/Transitive_Closure.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Oct 03 13:01:31 2024 +0200
@@ -64,6 +64,36 @@
tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
+bundle no_rtrancl_syntax
+begin
+no_notation
+ rtrancl (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999) and
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000)
+no_notation (ASCII)
+ rtrancl (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
+ rtranclp (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000)
+end
+
+bundle no_trancl_syntax
+begin
+no_notation
+ trancl (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
+no_notation (ASCII)
+ trancl (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
+ tranclp (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000)
+end
+
+bundle no_reflcl_syntax
+begin
+no_notation
+ reflcl (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999) and
+ reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
+no_notation (ASCII)
+ reflcl (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
+ reflclp (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
+end
+
subsection \<open>Reflexive closure\<close>
--- a/src/HOL/ex/Code_Lazy_Demo.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy Thu Oct 03 13:01:31 2024 +0200
@@ -40,9 +40,7 @@
| LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
syntax
- "_llist" :: "args => 'a list" (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
-syntax_consts
- LCons
+ "_llist" :: "args => 'a list" (\<open>(\<open>indent=1 notation=\<open>mixfix lazy list enumeration\<close>\<close>\<^bold>\<lbrakk>_\<^bold>\<rbrakk>)\<close>)
translations
"\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
"\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
--- a/src/Pure/Isar/bundle.ML Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Pure/Isar/bundle.ML Thu Oct 03 13:01:31 2024 +0200
@@ -13,11 +13,6 @@
val read: Proof.context -> xstring * Position.T -> Attrib.thms
val extern: Proof.context -> string -> xstring
val print_bundles: bool -> Proof.context -> unit
- val bundle: binding * Attrib.thms ->
- (binding * typ option * mixfix) list -> local_theory -> local_theory
- val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
- (binding * string option * mixfix) list -> local_theory -> local_theory
- val init: binding -> theory -> local_theory
val unbundle: name list -> local_theory -> local_theory
val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
val includes: name list -> Proof.context -> Proof.context
@@ -26,6 +21,11 @@
val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val including: name list -> Proof.state -> Proof.state
val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+ val bundle: {open_bundle: bool} -> binding * Attrib.thms ->
+ (binding * typ option * mixfix) list -> local_theory -> local_theory
+ val bundle_cmd: {open_bundle: bool} -> binding * (Facts.ref * Token.src list) list ->
+ (binding * string option * mixfix) list -> local_theory -> local_theory
+ val init: {open_bundle: bool} -> binding -> theory -> local_theory
end;
structure Bundle: BUNDLE =
@@ -53,6 +53,7 @@
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
+val get_global = Name_Space.get o get_all_generic o Context.Theory;
val get = Name_Space.get o get_all_generic o Context.Proof;
fun read ctxt = get ctxt o check ctxt;
@@ -60,6 +61,19 @@
fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
+(* context and morphisms *)
+
+val trim_context_bundle =
+ map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+
+fun transfer_bundle thy =
+ map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+
+fun transform_bundle phi =
+ map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+
+
+
(* target -- bundle under construction *)
fun the_target thy =
@@ -93,18 +107,51 @@
-(** define bundle **)
+(** open bundles **)
+
+fun apply_bundle loc bundle ctxt =
+ let val notes = if loc then Local_Theory.notes else Attrib.local_notes "" in
+ ctxt
+ |> Context_Position.set_visible false
+ |> notes [(Binding.empty_atts, bundle)] |> snd
+ |> Context_Position.restore_visible ctxt
+ end;
-(* context and morphisms *)
+local
+
+fun gen_unbundle loc prep args ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val bundle = maps (prep ctxt) args |> transfer_bundle thy;
+ in apply_bundle loc bundle ctxt end;
+
+fun gen_includes prep = gen_unbundle false prep;
+
+fun gen_include prep bs =
+ Proof.assert_forward #> Proof.map_context (gen_includes prep bs) #> Proof.reset_facts;
-val trim_context_bundle =
- map (fn (fact, atts) => (map Thm.trim_context fact, (map o map) Token.trim_context atts));
+fun gen_including prep bs =
+ Proof.assert_backward #> Proof.map_context (gen_includes prep bs);
+
+in
+
+val unbundle = gen_unbundle true get;
+val unbundle_cmd = gen_unbundle true read;
+
+val includes = gen_includes get;
+val includes_cmd = gen_includes read;
-fun transfer_bundle thy =
- map (fn (fact, atts) => (map (Thm.transfer thy) fact, (map o map) (Token.transfer thy) atts));
+val include_ = gen_include get;
+val include_cmd = gen_include read;
+
+val including = gen_including get;
+val including_cmd = gen_including read;
-fun transform_bundle phi =
- map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+end;
+
+
+
+(** define bundle **)
fun define_bundle (b, bundle) context =
let
@@ -118,7 +165,7 @@
local
-fun gen_bundle prep_fact prep_att add_fixes (binding, raw_bundle) raw_fixes lthy =
+fun gen_bundle prep_fact prep_att add_fixes {open_bundle} (binding, raw_bundle) raw_fixes lthy =
let
val (_, ctxt') = add_fixes raw_fixes lthy;
val bundle0 = raw_bundle
@@ -133,6 +180,7 @@
(fn phi => fn context =>
let val psi = Morphism.set_trim_context'' context phi
in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
+ |> open_bundle ? apply_bundle true bundle
end;
in
@@ -149,22 +197,29 @@
fun bad_operation _ = error "Not possible in bundle target";
-fun conclude invisible binding =
+fun conclude {open_bundle, invisible} binding =
Local_Theory.background_theory_result (fn thy =>
- thy
- |> invisible ? Context_Position.set_visible_global false
- |> Context.Theory
- |> define_bundle (binding, the_target thy)
- ||> (Context.the_theory
- #> invisible ? Context_Position.restore_visible_global thy
- #> reset_target));
+ let
+ val (name, thy') = thy
+ |> invisible ? Context_Position.set_visible_global false
+ |> Context.Theory
+ |> define_bundle (binding, the_target thy)
+ ||> Context.the_theory;
+ val bundle = get_global thy' name;
+ val thy'' = thy'
+ |> open_bundle ?
+ (Context_Position.set_visible_global false #>
+ Attrib.global_notes "" [(Binding.empty_atts, bundle)] #> snd)
+ |> Context_Position.restore_visible_global thy
+ |> reset_target;
+ in (name, thy'') end);
fun pretty binding lthy =
let
val bundle = the_target (Proof_Context.theory_of lthy);
val (name, lthy') = lthy
|> Local_Theory.raw_theory (Context_Position.set_visible_global false)
- |> conclude true binding;
+ |> conclude {open_bundle = false, invisible = true} binding;
val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
val markup_name =
Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_all thy_ctxt')) name;
@@ -189,12 +244,12 @@
in
-fun init binding thy =
+fun init {open_bundle} binding thy =
thy
|> Local_Theory.init
{background_naming = Sign.naming_of thy,
setup = set_target [] #> Proof_Context.init_global,
- conclude = conclude false binding #> #2}
+ conclude = conclude {open_bundle = open_bundle, invisible = false} binding #> #2}
{define = bad_operation,
notes = bundle_notes,
abbrev = bad_operation,
@@ -205,47 +260,4 @@
end;
-
-
-(** activate bundles **)
-
-local
-
-fun gen_activate notes prep_bundle args ctxt =
- let
- val thy = Proof_Context.theory_of ctxt;
- val decls = maps (prep_bundle ctxt) args |> transfer_bundle thy;
- in
- ctxt
- |> Context_Position.set_visible false
- |> notes [(Binding.empty_atts, decls)] |> #2
- |> Context_Position.restore_visible ctxt
- end;
-
-fun gen_unbundle prep_bundle = gen_activate Local_Theory.notes prep_bundle;
-
-fun gen_includes prep_bundle = gen_activate (Attrib.local_notes "") prep_bundle;
-
-fun gen_include prep_bundle bs =
- Proof.assert_forward #> Proof.map_context (gen_includes prep_bundle bs) #> Proof.reset_facts;
-
-fun gen_including prep_bundle bs =
- Proof.assert_backward #> Proof.map_context (gen_includes prep_bundle bs)
-
-in
-
-val unbundle = gen_unbundle get;
-val unbundle_cmd = gen_unbundle read;
-
-val includes = gen_includes get;
-val includes_cmd = gen_includes read;
-
-val include_ = gen_include get;
-val include_cmd = gen_include read;
-
-val including = gen_including get;
-val including_cmd = gen_including read;
-
end;
-
-end;
--- a/src/Pure/Pure.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/Pure/Pure.thy Thu Oct 03 13:01:31 2024 +0200
@@ -37,7 +37,7 @@
"declaration" "syntax_declaration"
"parse_ast_translation" "parse_translation" "print_translation"
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
- and "bundle" :: thy_decl_block
+ and "bundle" "open_bundle" :: thy_decl_block
and "unbundle" :: thy_decl
and "include" "including" :: prf_decl
and "print_bundles" :: diag
@@ -637,26 +637,34 @@
ML \<open>
local
+fun bundle_cmd open_bundle =
+ (Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
+ >> (uncurry (Bundle.bundle_cmd {open_bundle = open_bundle}));
+
+fun bundle_begin open_bundle =
+ Parse.binding --| Parse.begin >> Bundle.init {open_bundle = open_bundle};
+
val _ =
Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>bundle\<close>
- "define bundle of declarations"
- ((Parse.binding --| \<^keyword>\<open>=\<close>) -- Parse.thms1 -- Parse.for_fixes
- >> (uncurry Bundle.bundle_cmd))
- (Parse.binding --| Parse.begin >> Bundle.init);
+ "define bundle of declarations" (bundle_cmd false) (bundle_begin false);
+
+val _ =
+ Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\<open>open_bundle\<close>
+ "define and open bundle of declarations" (bundle_cmd true) (bundle_begin true);
val _ =
Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
- "activate declarations from bundle in local theory"
+ "open bundle in local theory"
(Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
val _ =
Outer_Syntax.command \<^command_keyword>\<open>include\<close>
- "activate declarations from bundle in proof body"
+ "open bundle in proof body"
(Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>including\<close>
- "activate declarations from bundle in goal refinement"
+ "open bundle in goal refinement"
(Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
val _ =
--- a/src/ZF/Induct/Multiset.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy Thu Oct 03 13:01:31 2024 +0200
@@ -75,8 +75,6 @@
syntax
"_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{# _ \<in> _./ _#})\<close>)
-syntax_consts
- MCollect
translations
"{#x \<in> M. P#}" == "CONST MCollect(M, \<lambda>x. P)"
--- a/src/ZF/List.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/List.thy Thu Oct 03 13:01:31 2024 +0200
@@ -16,9 +16,7 @@
notation Nil (\<open>[]\<close>)
syntax
- "_List" :: "is \<Rightarrow> i" (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
-syntax_consts
- Cons
+ "_List" :: "is \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
translations
"[x, xs]" == "CONST Cons(x, [xs])"
"[x]" == "CONST Cons(x, [])"
--- a/src/ZF/ZF_Base.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/ZF_Base.thy Thu Oct 03 13:01:31 2024 +0200
@@ -56,8 +56,6 @@
syntax
"_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
-syntax_consts
- Replace
translations
"{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
@@ -69,8 +67,6 @@
syntax
"_RepFun" :: "[i, pttrn, i] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix functional replacement\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
-syntax_consts
- RepFun
translations
"{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
@@ -81,8 +77,6 @@
syntax
"_Collect" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ \<in> _ ./ _})\<close>)
-syntax_consts
- Collect
translations
"{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
@@ -133,9 +127,7 @@
syntax
"" :: "i \<Rightarrow> is" (\<open>_\<close>)
"_Enum" :: "[i, is] \<Rightarrow> is" (\<open>_,/ _\<close>)
- "_Finset" :: "is \<Rightarrow> i" (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
-syntax_consts
- cons
+ "_Finset" :: "is \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix set enumeration\<close>\<close>{_})\<close>)
translations
"{x, xs}" == "CONST cons(x, {xs})"
"{x}" == "CONST cons(x, 0)"
@@ -196,9 +188,7 @@
syntax
"" :: "i \<Rightarrow> tuple_args" (\<open>_\<close>)
"_Tuple_args" :: "[i, tuple_args] \<Rightarrow> tuple_args" (\<open>_,/ _\<close>)
- "_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open>\<langle>(\<open>notation=\<open>mixfix tuple enumeration\<close>\<close>_,/ _)\<rangle>\<close>)
-syntax_consts
- Pair
+ "_Tuple" :: "[i, tuple_args] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix tuple enumeration\<close>\<close>\<langle>_,/ _\<rangle>)\<close>)
translations
"\<langle>x, y, z\<rangle>" == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
"\<langle>x, y\<rangle>" == "CONST Pair(x, y)"
--- a/src/ZF/func.thy Wed Oct 02 18:32:36 2024 +0200
+++ b/src/ZF/func.thy Thu Oct 03 13:01:31 2024 +0200
@@ -452,8 +452,6 @@
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
-syntax_consts
- update
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
"f(x:=y)" == "CONST update(f,x,y)"