diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/Imperative_HOL/ex/SatChecker.thy
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Thu May 26 17:51:22 2016 +0200
@@ -2,22 +2,22 @@
     Author:     Lukas Bulwahn, TU Muenchen
 *)
 
-section {* An efficient checker for proofs from a SAT solver *}
+section \<open>An efficient checker for proofs from a SAT solver\<close>
 
 theory SatChecker
 imports "~~/src/HOL/Library/RBT_Impl" Sorted_List "../Imperative_HOL"
 begin
 
-section{* General settings and functions for our representation of clauses *}
+section\<open>General settings and functions for our representation of clauses\<close>
 
-subsection{* Types for Literals, Clauses and ProofSteps *}
-text {* We encode Literals as integers and Clauses as sorted Lists. *}
+subsection\<open>Types for Literals, Clauses and ProofSteps\<close>
+text \<open>We encode Literals as integers and Clauses as sorted Lists.\<close>
 
 type_synonym ClauseId = nat
 type_synonym Lit = int
 type_synonym Clause = "Lit list"
 
-text {* This resembles exactly to Isat's Proof Steps *}
+text \<open>This resembles exactly to Isat's Proof Steps\<close>
 
 type_synonym Resolvants = "ClauseId * (Lit * ClauseId) list"
 datatype ProofStep =
@@ -27,8 +27,8 @@
   | Delete ClauseId
   | Xstep ClauseId ClauseId
 
-subsection{* Interpretation of Literals, Clauses, and an array of Clauses *} 
-text {* Specific definitions for Literals as integers *}
+subsection\<open>Interpretation of Literals, Clauses, and an array of Clauses\<close> 
+text \<open>Specific definitions for Literals as integers\<close>
 
 definition compl :: "Lit \<Rightarrow> Lit"
 where
@@ -54,7 +54,7 @@
 lemma compl_exists: "\<exists>l'. l = compl l'"
 unfolding compl_def by arith
 
-text {* Specific definitions for Clauses as sorted lists *}
+text \<open>Specific definitions for Clauses as sorted lists\<close>
 
 definition interpClause :: "(nat \<Rightarrow> bool) \<Rightarrow> Clause \<Rightarrow> bool"
 where
@@ -116,12 +116,12 @@
 unfolding inconsistent_def correctClause_def
 by auto
 
-text {* Specific definition for derived clauses in the Array *}
+text \<open>Specific definition for derived clauses in the Array\<close>
 
 definition
   array_ran :: "('a::heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
   "array_ran a h = {e. Some e \<in> set (Array.get h a)}"
-    -- {*FIXME*}
+    \<comment> \<open>FIXME\<close>
 
 lemma array_ranI: "\<lbrakk> Some b = Array.get h a ! i; i < Array.length h a \<rbrakk> \<Longrightarrow> b \<in> array_ran a h"
 unfolding array_ran_def Array.length_def by simp
@@ -165,11 +165,11 @@
   by auto
 
 
-section{* Improved version of SatChecker *}
+section\<open>Improved version of SatChecker\<close>
 
-text{* This version just uses a single list traversal. *}
+text\<open>This version just uses a single list traversal.\<close>
 
-subsection{* Function definitions *}
+subsection\<open>Function definitions\<close>
 
 primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where
@@ -209,7 +209,7 @@
 
 declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del]
 
-subsection {* Proofs about these functions *}
+subsection \<open>Proofs about these functions\<close>
 
 lemma res_mem:
 assumes "effect (res_mem l xs) h h' r"
@@ -408,7 +408,7 @@
     done
 qed
 
-subsection {* res_thm and doProofStep *}
+subsection \<open>res_thm and doProofStep\<close>
 
 definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
 where
@@ -598,9 +598,9 @@
 apply (drule bspec)
 by (rule array_ranI, auto)
 
-section {* Functional version with Lists as Array *}
+section \<open>Functional version with Lists as Array\<close>
 
-subsection {* List specific definitions *}
+subsection \<open>List specific definitions\<close>
 
 definition list_ran :: "'a option list \<Rightarrow> 'a set"
 where
@@ -636,7 +636,7 @@
   "correctList rootcls xs =
   (\<forall>cl \<in> list_ran xs. correctClause rootcls cl \<and> sorted cl \<and> distinct cl)"
 
-subsection {* Checker functions *}
+subsection \<open>Checker functions\<close>
 
 primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap" 
 where
@@ -670,7 +670,7 @@
   }"
 
 
-section {* Functional version with RedBlackTrees *}
+section \<open>Functional version with RedBlackTrees\<close>
 
 primrec tres_thm :: "(ClauseId, Clause) RBT_Impl.rbt \<Rightarrow> Lit \<times> ClauseId \<Rightarrow> Clause \<Rightarrow> Clause Heap"
 where