src/HOL/ex/Refute_Examples.thy

 
 lemma "(x == Pure.all) \<Longrightarrow> False"
 refute [expect = genuine]
 oops
 
-lemma "(x == (op ==)) \<Longrightarrow> False"
-refute [expect = genuine]
-oops
-
-lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
+lemma "(x == (==)) \<Longrightarrow> False"
+refute [expect = genuine]
+oops
+
+lemma "(x == (\<Longrightarrow>)) \<Longrightarrow> False"
 refute [expect = genuine]
 oops
 
 (*****************************************************************************)
 

 
 lemma "x : {x. P x}"
 refute
 oops
 
-lemma "P op:"
-refute
-oops
-
-lemma "P (op: x)"
+lemma "P (:)"
+refute
+oops
+
+lemma "P ((:) x)"
 refute
 oops
 
 lemma "P Collect"
 refute