src/HOL/Quickcheck_Examples/Completeness.thy

--- a/src/HOL/Quickcheck_Examples/Completeness.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Completeness.thy	Thu May 26 17:51:22 2016 +0200
@@ -3,13 +3,13 @@
     Copyright   2012 TU Muenchen
 *)
 
-section {* Proving completeness of exhaustive generators *}
+section \<open>Proving completeness of exhaustive generators\<close>
 
 theory Completeness
 imports Main
 begin
 
-subsection {* Preliminaries *}
+subsection \<open>Preliminaries\<close>
 
 primrec is_some
 where
@@ -22,7 +22,7 @@
 
 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 
-subsection {* Defining the size of values *}
+subsection \<open>Defining the size of values\<close>
 
 hide_const size
 
@@ -74,7 +74,7 @@
 
 end
 
-subsection {* Completeness *}
+subsection \<open>Completeness\<close>
 
 class complete = exhaustive + size +
 assumes
@@ -89,7 +89,7 @@
   obtains v where "size (v :: 'a :: complete) \<le> n" "is_some (f v)"
 using assms by (metis complete)
 
-subsubsection {* Instance Proofs *}
+subsubsection \<open>Instance Proofs\<close>
 
 declare exhaustive_int'.simps [simp del]