--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Wed Dec 30 21:57:52 2015 +0100
@@ -6,13 +6,13 @@
imports Main
begin
-subsubsection {* Logic *}
+subsubsection \<open>Logic\<close>
lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)"
by blast
-subsection {* Sets *}
+subsection \<open>Sets\<close>
lemma set_lemmas:
"f(x) : (UN x. {f(x)})"
@@ -22,7 +22,7 @@
by auto
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
by (simp add: diff_Suc split add: nat.split)