src/HOL/UNITY/Comp.thy

--- a/src/HOL/UNITY/Comp.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp.thy	Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
 Technical Report 2000-003, University of Florida, 2000.
 *)
 
-section{*Composition: Basic Primitives*}
+section\<open>Composition: Basic Primitives\<close>
 
 theory Comp
 imports Union
@@ -42,7 +42,7 @@
   where "funPair f g == %x. (f x, g x)"
 
 
-subsection{*The component relation*}
+subsection\<open>The component relation\<close>
 lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)"
 apply (unfold component_def, auto)
 apply (rule_tac x = "G\<squnion>Ga" in exI)
@@ -115,7 +115,7 @@
 lemmas program_less_le = strict_component_def
 
 
-subsection{*The preserves property*}
+subsection\<open>The preserves property\<close>
 
 lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
 by (unfold preserves_def, blast)