diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- 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>"