--- a/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Wed Jan 10 15:25:09 2018 +0100
@@ -318,7 +318,7 @@
nitpick [expect = none]
by auto
-lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
+lemma "x \<equiv> (\<equiv>) \<Longrightarrow> False"
nitpick [card = 1, expect = genuine]
oops
@@ -334,11 +334,11 @@
nitpick [card = 1-10, expect = none]
by auto
-lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
+lemma "x \<equiv> (\<Longrightarrow>) \<Longrightarrow> False"
nitpick [expect = genuine]
oops
-lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))"
+lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> ((\<Longrightarrow>) x) \<equiv> (\<lambda>y. ((\<Longrightarrow>) x (I y)))"
nitpick [expect = none]
by auto
@@ -458,8 +458,8 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x. op \<and> (I x))"
- "I = (\<lambda>x. x) \<Longrightarrow> (op \<and>) = (\<lambda>x y. x \<and> (I y))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (\<and>) = (\<lambda>x. (\<and>) (I x))"
+ "I = (\<lambda>x. x) \<Longrightarrow> (\<and>) = (\<lambda>x y. x \<and> (I y))"
nitpick [expect = none]
by auto
@@ -471,7 +471,7 @@
nitpick [expect = none]
by auto
-lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
+lemma "(\<longrightarrow>) = (\<lambda>x. (\<longrightarrow>) x)" "((\<longrightarrow>) ) = (\<lambda>x y. x \<longrightarrow> y)"
nitpick [expect = none]
by auto
@@ -583,7 +583,7 @@
nitpick [expect = genuine]
oops
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (\<in>) = (\<lambda>x. ((\<in>) (I x)))"
nitpick [expect = none]
apply (rule ext)
apply (rule ext)
@@ -610,7 +610,7 @@
nitpick [card = 1-5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (\<union>) = (\<lambda>x. (\<union>) (I x))"
nitpick [card = 1-5, expect = none]
by auto
@@ -618,7 +618,7 @@
nitpick [expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (\<inter>) = (\<lambda>x. (\<inter>) (I x))"
nitpick [card = 1-5, expect = none]
by auto
@@ -630,7 +630,7 @@
nitpick [card = 1-5, expect = none]
by auto
-lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
+lemma "I = (\<lambda>x. x) \<Longrightarrow> (\<subset>) = (\<lambda>x. (\<subset>) (I x))"
nitpick [card = 1-5, expect = none]
by auto