# HG changeset patch
# User paulson
# Date 1536768753 -3600
# Node ID e2244e5707dd9ab809c753defbef24ce658d3b73
# Parent  271026e97ca2f39aaf98d1f34a292a8720f8a234# Parent  26be7c0d65a1d67d2d92cf05d857d5cc3c78b70c
merged

diff -r 26be7c0d65a1 -r e2244e5707dd src/HOL/Data_Structures/Sorting.thy
--- 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"
diff -r 26be7c0d65a1 -r e2244e5707dd src/HOL/HOL.thy
--- 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)