src/HOL/Library/Heap.thy
changeset 26586 a2255b130fd9
parent 26300 03def556e26e
child 26817 9217577e0a23
equal deleted inserted replaced
26585:3bf2ebb7148e 26586:a2255b130fd9
   132 
   132 
   133 subsection {* Imperative references and arrays *}
   133 subsection {* Imperative references and arrays *}
   134 
   134 
   135 text {*
   135 text {*
   136   References and arrays are developed in parallel,
   136   References and arrays are developed in parallel,
   137   but keeping them seperate makes some later proofs simpler.
   137   but keeping them separate makes some later proofs simpler.
   138 *}
   138 *}
   139 
   139 
   140 subsubsection {* Primitive operations *}
   140 subsubsection {* Primitive operations *}
   141 
   141 
   142 definition
   142 definition