# HG changeset patch
# User wenzelm
# Date 1728395051 -7200
# Node ID 5b201b24d99bec339f336b5c86b751eb4d81b2a9
# Parent  12990a6dddcb01059fc6660e2d97932b79411907
tuned whitespace, to simplify hypersearch;

diff -r 12990a6dddcb -r 5b201b24d99b src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -360,9 +360,7 @@
       "[x, xs]" == "x # [xs]"
       "[x]" == "x # []"
 
-    no_notation
-      Nil (\<open>[]\<close>) and
-      Cons (infixr \<open>#\<close> 65)
+    no_notation Nil  (\<open>[]\<close>) and Cons  (infixr \<open>#\<close> 65)
 
     hide_type list
     hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
diff -r 12990a6dddcb -r 5b201b24d99b src/Doc/Tutorial/ToyList/ToyList.thy
--- a/src/Doc/Tutorial/ToyList/ToyList.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -9,7 +9,7 @@
 the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
 \<close>
 
-no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
+no_notation Nil  ("[]") and Cons  (infixr "#" 65) and append  (infixr "@" 65)
 hide_type list
 hide_const rev
 
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -1853,8 +1853,7 @@
   shows "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> Measurable.pred M (\<lambda>w. f w < g w)"
   unfolding Measurable.pred_def by (rule borel_measurable_less)
 
-no_notation
-  eucl_less (infix \<open><e\<close> 50)
+no_notation eucl_less  (infix \<open><e\<close> 50)
 
 lemma borel_measurable_Max2[measurable (raw)]:
   fixes f::"_ \<Rightarrow> _ \<Rightarrow> 'a::{second_countable_topology, dense_linorder, linorder_topology}"
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -288,8 +288,7 @@
   shows "compact {a .. b}"
   by (metis compact_cbox interval_cbox)
 
-no_notation
-  eucl_less (infix \<open><e\<close> 50)
+no_notation eucl_less  (infix \<open><e\<close> 50)
 
 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
   by (auto intro: sum_nonneg)
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -2484,7 +2484,6 @@
   qed
 qed auto
 
-no_notation
-  eucl_less (infix \<open><e\<close> 50)
+no_notation eucl_less  (infix \<open><e\<close> 50)
 
 end
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Examples/Coherent.thy
--- a/src/HOL/Examples/Coherent.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Examples/Coherent.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -11,9 +11,7 @@
 
 subsection \<open>Equivalence of two versions of Pappus' Axiom\<close>
 
-no_notation
-  comp (infixl \<open>o\<close> 55) and
-  relcomp (infixr \<open>O\<close> 75)
+no_notation comp  (infixl \<open>o\<close> 55) and relcomp  (infixr \<open>O\<close> 75)
 
 lemma p1p2:
   assumes "col a b c l \<and> col d e f m"
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Induct/SList.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -83,9 +83,7 @@
 no_translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
-no_notation
-  Nil  (\<open>[]\<close>) and
-  Cons (infixr \<open>#\<close> 65)
+no_notation Nil  (\<open>[]\<close>) and Cons  (infixr \<open>#\<close> 65)
 
 definition
   Nil       :: "'a list"                               (\<open>[]\<close>) where
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -1957,7 +1957,7 @@
 
 end
 
-no_notation Quickcheck_Exhaustive.orelse (infixr \<open>orelse\<close> 55)
+no_notation Quickcheck_Exhaustive.orelse  (infixr \<open>orelse\<close> 55)
 
 instantiation fset :: (random) random
 begin
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Predicate.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -727,8 +727,7 @@
   "pred_of_set (set xs) = foldr sup (List.map Predicate.single xs) bot"
   by (simp add: pred_of_set_set_fold_sup ac_simps foldr_fold fun_eq_iff)
 
-no_notation
-  bind (infixl \<open>\<bind>\<close> 70)
+no_notation bind  (infixl \<open>\<bind>\<close> 70)
 
 hide_type (open) pred seq
 hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -219,7 +219,7 @@
 abbreviation joint_probability (\<open>\<P>'(_ ; _') _\<close>) where
   "\<P>(X ; Y) x \<equiv> \<P>(\<lambda>x. (X x, Y x)) x"
 
-no_notation disj (infixr \<open>|\<close> 30)
+no_notation disj  (infixr \<open>|\<close> 30)
 
 abbreviation conditional_probability (\<open>\<P>'(_ | _') _\<close>) where
   "\<P>(X | Y) x \<equiv> (\<P>(X ; Y) x) / \<P>(Y) (snd`x)"
diff -r 12990a6dddcb -r 5b201b24d99b src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/HOL/Quotient.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -745,8 +745,7 @@
   \<open>Scan.succeed Quotient_Tacs.lifted_attrib\<close>
   \<open>lift theorems to quotient types\<close>
 
-no_notation
-  rel_conj (infixr \<open>OOO\<close> 75)
+no_notation rel_conj  (infixr \<open>OOO\<close> 75)
 
 section \<open>Lifting of BNFs\<close>
 
diff -r 12990a6dddcb -r 5b201b24d99b src/ZF/ex/Ring.thy
--- a/src/ZF/ex/Ring.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/ZF/ex/Ring.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -6,9 +6,7 @@
 
 theory Ring imports Group begin
 
-no_notation
-  cadd  (infixl \<open>\<oplus>\<close> 65) and
-  cmult  (infixl \<open>\<otimes>\<close> 70)
+no_notation cadd  (infixl \<open>\<oplus>\<close> 65) and cmult  (infixl \<open>\<otimes>\<close> 70)
 
 (*First, we must simulate a record declaration:
 record ring = monoid +