--- 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
--- 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
--- 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}"
--- 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)
--- 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
--- 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"
--- 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
--- 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
--- 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
--- 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)"
--- 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>
--- 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 +