--- a/src/HOL/Data_Structures/Sorting.thy Wed Sep 12 12:51:52 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy Wed Sep 12 17:12:33 2018 +0100
@@ -309,7 +309,8 @@
"c_msort_bu xs = c_merge_all (map (\<lambda>x. [x]) xs)"
lemma length_merge_adj:
- "\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
+ "\<lbrakk> even(length xss); \<forall>xs \<in> set xss. length xs = m \<rbrakk>
+ \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m"
by(induction xss rule: merge_adj.induct) (auto simp: length_merge)
lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss"
--- a/src/HOL/HOL.thy Wed Sep 12 12:51:52 2018 +0100
+++ b/src/HOL/HOL.thy Wed Sep 12 17:12:33 2018 +0100
@@ -81,9 +81,16 @@
judgment Trueprop :: "bool \<Rightarrow> prop" ("(_)" 5)
axiomatization implies :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longrightarrow>" 25)
- and eq :: "['a, 'a] \<Rightarrow> bool" (infixl "=" 50)
+ and eq :: "['a, 'a] \<Rightarrow> bool"
and The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
+notation (input)
+ eq (infixl "=" 50)
+notation (output)
+ eq (infix "=" 50)
+
+text \<open>The input syntax for \<open>eq\<close> is more permissive than the output syntax
+because of the large amount of material that relies on infixl.\<close>
subsubsection \<open>Defined connectives and quantifiers\<close>
@@ -134,22 +141,15 @@
"\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
-abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infixl "\<noteq>" 50)
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool" (infix "\<noteq>" 50)
where "x \<noteq> y \<equiv> \<not> (x = y)"
-notation (output)
- eq (infix "=" 50) and
- not_equal (infix "\<noteq>" 50)
-
-notation (ASCII output)
- not_equal (infix "~=" 50)
-
notation (ASCII)
Not ("~ _" [40] 40) and
conj (infixr "&" 35) and
disj (infixr "|" 30) and
implies (infixr "-->" 25) and
- not_equal (infixl "~=" 50)
+ not_equal (infix "~=" 50)
abbreviation (iff)
iff :: "[bool, bool] \<Rightarrow> bool" (infixr "\<longleftrightarrow>" 25)