--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Thu May 26 17:51:22 2016 +0200
@@ -9,8 +9,8 @@
declare [[quickcheck_finite_type_size=5]]
-text {* We show how other default types help to find counterexamples to propositions if
- the standard default type @{typ int} is insufficient. *}
+text \<open>We show how other default types help to find counterexamples to propositions if
+ the standard default type @{typ int} is insufficient.\<close>
notation
less_eq (infix "\<sqsubseteq>" 50) and
@@ -22,7 +22,7 @@
declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
-subsection {* Distributive lattices *}
+subsection \<open>Distributive lattices\<close>
lemma sup_inf_distrib2:
"((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
@@ -49,7 +49,7 @@
quickcheck[expect = counterexample]
oops
-subsection {* Bounded lattices *}
+subsection \<open>Bounded lattices\<close>
lemma inf_bot_left [simp]:
"\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"