--- a/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Sat Jan 05 17:24:33 2019 +0100
@@ -10,7 +10,7 @@
declare [[quickcheck_finite_type_size=5]]
text \<open>We show how other default types help to find counterexamples to propositions if
- the standard default type @{typ int} is insufficient.\<close>
+ the standard default type \<^typ>\<open>int\<close> is insufficient.\<close>
notation
less_eq (infix "\<sqsubseteq>" 50) and