# HG changeset patch
# User wenzelm
# Date 1727861239 -7200
# Node ID 6ae3d0b2b8ad8358636147100031fac449766936
# Parent  9dde09c065e1aa74d1fbd41bfd160597602e0ae3
tuned whitespace;

diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Analysis/Cross3.thy
--- a/src/HOL/Analysis/Cross3.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy	Wed Oct 02 11:27:19 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
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -20,16 +20,14 @@
 
 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)
+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
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -461,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
 
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Analysis/Lipschitz.thy
--- a/src/HOL/Analysis/Lipschitz.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -12,10 +12,12 @@
 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
+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
 
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Oct 02 11:27:19 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
 
 
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Combinatorics/Perm.thy
--- a/src/HOL/Combinatorics/Perm.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -794,16 +794,16 @@
 
 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
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -1143,7 +1143,8 @@
 
 section "Avoid pollution of name space"
 
-bundle floatarith_notation begin
+bundle floatarith_notation
+begin
 
 notation Add (\<open>Add\<close>)
 notation Minus (\<open>Minus\<close>)
@@ -1166,7 +1167,8 @@
 
 end
 
-bundle no_floatarith_notation begin
+bundle no_floatarith_notation
+begin
 
 no_notation Add (\<open>Add\<close>)
 no_notation Minus (\<open>Minus\<close>)
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 02 11:27:19 2024 +0200
@@ -803,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
@@ -1005,10 +1003,13 @@
   where "A \<times> B \<equiv> Sigma A (\<lambda>_. B)"
 end
 
-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
 
diff -r 9dde09c065e1 -r 6ae3d0b2b8ad src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Transfer.thy	Wed Oct 02 11:27:19 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