diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
 From Misra, "A Logic for Concurrent Programming", 1994.
 *)
 
-section {*The Basic UNITY Theory*}
+section \<open>The Basic UNITY Theory\<close>
 
 theory UNITY imports Main begin
 
@@ -54,11 +54,11 @@
     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
 
 definition increasing :: "['a => 'b::{order}] => 'a program set" where
-    --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
+    \<comment>\<open>Polymorphic in both states and the meaning of \<open>\<le>\<close>\<close>
     "increasing f == \<Inter>z. stable {s. z \<le> f s}"
 
 
-subsubsection{*The abstract type of programs*}
+subsubsection\<open>The abstract type of programs\<close>
 
 lemmas program_typedef =
      Rep_Program Rep_Program_inverse Abs_Program_inverse 
@@ -83,7 +83,7 @@
 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
 by (simp add: insert_absorb)
 
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
 
 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
 by (simp add: program_typedef)
@@ -95,7 +95,7 @@
      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
 by (simp add: program_typedef)
 
-subsubsection{*Equality for UNITY programs*}
+subsubsection\<open>Equality for UNITY programs\<close>
 
 lemma surjective_mk_program [simp]:
      "mk_program (Init F, Acts F, AllowedActs F) = F"
@@ -124,7 +124,7 @@
 by (blast intro: program_equalityI program_equalityE)
 
 
-subsubsection{*co*}
+subsubsection\<open>co\<close>
 
 lemma constrainsI: 
     "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
@@ -147,12 +147,12 @@
 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
 by (unfold constrains_def, blast)
 
-text{*monotonic in 2nd argument*}
+text\<open>monotonic in 2nd argument\<close>
 lemma constrains_weaken_R: 
     "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
 by (unfold constrains_def, blast)
 
-text{*anti-monotonic in 1st argument*}
+text\<open>anti-monotonic in 1st argument\<close>
 lemma constrains_weaken_L: 
     "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
 by (unfold constrains_def, blast)
@@ -161,7 +161,7 @@
    "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
 by (unfold constrains_def, blast)
 
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
 
 lemma constrains_Un: 
     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
@@ -184,7 +184,7 @@
 lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
 by (unfold constrains_def, blast)
 
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
 
 lemma constrains_Int: 
     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
@@ -198,8 +198,8 @@
 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
 by (unfold constrains_def, auto)
 
-text{*The reasoning is by subsets since "co" refers to single actions
-  only.  So this rule isn't that useful.*}
+text\<open>The reasoning is by subsets since "co" refers to single actions
+  only.  So this rule isn't that useful.\<close>
 lemma constrains_trans: 
     "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
 by (unfold constrains_def, blast)
@@ -209,7 +209,7 @@
 by (unfold constrains_def, clarify, blast)
 
 
-subsubsection{*unless*}
+subsubsection\<open>unless\<close>
 
 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
 by (unfold unless_def, assumption)
@@ -218,7 +218,7 @@
 by (unfold unless_def, assumption)
 
 
-subsubsection{*stable*}
+subsubsection\<open>stable\<close>
 
 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
 by (unfold stable_def, assumption)
@@ -229,7 +229,7 @@
 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
 by (unfold stable_def constrains_def, auto)
 
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
 
 lemma stable_Un: 
     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
@@ -248,7 +248,7 @@
     "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
 by (unfold stable_def constrains_def, blast)
 
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
 
 lemma stable_Int: 
     "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
@@ -278,18 +278,18 @@
 lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
 
 
-subsubsection{*invariant*}
+subsubsection\<open>invariant\<close>
 
 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
 by (simp add: invariant_def)
 
-text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
+text\<open>Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}\<close>
 lemma invariant_Int:
      "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
 by (auto simp add: invariant_def stable_Int)
 
 
-subsubsection{*increasing*}
+subsubsection\<open>increasing\<close>
 
 lemma increasingD: 
      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
@@ -319,15 +319,15 @@
      ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
-text{*As above, but for the trivial case of a one-variable state, in which the
-  state is identified with its one variable.*}
+text\<open>As above, but for the trivial case of a one-variable state, in which the
+  state is identified with its one variable.\<close>
 lemma elimination_sing: 
     "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
 
 
-subsubsection{*Theoretical Results from Section 6*}
+subsubsection\<open>Theoretical Results from Section 6\<close>
 
 lemma constrains_strongest_rhs: 
     "F \<in> A co (strongest_rhs F A )"
@@ -338,7 +338,7 @@
 by (unfold constrains_def strongest_rhs_def, blast)
 
 
-subsubsection{*Ad-hoc set-theory rules*}
+subsubsection\<open>Ad-hoc set-theory rules\<close>
 
 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
 by blast
@@ -346,7 +346,7 @@
 lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
 by blast
 
-text{*Needed for WF reasoning in WFair.thy*}
+text\<open>Needed for WF reasoning in WFair.thy\<close>
 
 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
 by blast
@@ -355,7 +355,7 @@
 by blast
 
 
-subsection{*Partial versus Total Transitions*}
+subsection\<open>Partial versus Total Transitions\<close>
 
 definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
     "totalize_act act == act \<union> Id_on (-(Domain act))"
@@ -376,7 +376,7 @@
 by (blast intro: sym [THEN image_eqI])
 
 
-subsubsection{*Basic properties*}
+subsubsection\<open>Basic properties\<close>
 
 lemma totalize_act_Id [simp]: "totalize_act Id = Id"
 by (simp add: totalize_act_def) 
@@ -427,9 +427,9 @@
 by (simp add: mk_total_program_def)
 
 
-subsection{*Rules for Lazy Definition Expansion*}
+subsection\<open>Rules for Lazy Definition Expansion\<close>
 
-text{*They avoid expanding the full program, which is a large expression*}
+text\<open>They avoid expanding the full program, which is a large expression\<close>
 
 lemma def_prg_Init:
      "F = mk_total_program (init,acts,allowed) ==> Init F = init"
@@ -445,16 +445,16 @@
       ==> AllowedActs F = insert Id allowed"
 by (simp add: mk_total_program_def)
 
-text{*An action is expanded if a pair of states is being tested against it*}
+text\<open>An action is expanded if a pair of states is being tested against it\<close>
 lemma def_act_simp:
      "act = {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
 by (simp add: mk_total_program_def)
 
-text{*A set is expanded only if an element is being tested against it*}
+text\<open>A set is expanded only if an element is being tested against it\<close>
 lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
 by (simp add: mk_total_program_def)
 
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
 
 lemma Init_total_eq [simp]:
      "Init (mk_total_program (init,acts,allowed)) = init"