src/HOL/UNITY/Comp/AllocImpl.thy

 (*  Title:      HOL/UNITY/Comp/AllocImpl.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 *)
 
-section{*Implementation of a multiple-client allocator from a single-client allocator*}
+section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>
 
 theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
 
 
 (** State definitions.  OUTPUT variables are locals **)

 declare funPair_o_distrib [simp]
 declare Always_INT_distrib [simp]
 declare o_apply [simp del]
 
 
-subsection{*Theorems for Merge*}
+subsection\<open>Theorems for Merge\<close>
 
 context Merge
 begin
 
 lemma Merge_Allowed:

 done
 
 end
 
 
-subsection{*Theorems for Distributor*}
+subsection\<open>Theorems for Distributor\<close>
 
 context Distrib
 begin
 
 lemma Distr_Increasing_Out:

 done
 
 end
 
 
-subsection{*Theorems for Allocator*}
+subsection\<open>Theorems for Allocator\<close>
 
 lemma alloc_refinement_lemma:
      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
       \<subseteq> {s. (\<Sum>x \<in> lessThan n. f x) \<le> (\<Sum>x \<in> lessThan n. g x s)}"
 apply (induct_tac "n")