src/HOL/HOLCF/IOA/Storage/Impl.thy
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 62002 f1599e98c4d0
equal deleted inserted replaced
58879:143c85e3cdb5 58880:0baae4311a9f
     1 (*  Title:      HOL/HOLCF/IOA/Storage/Impl.thy
     1 (*  Title:      HOL/HOLCF/IOA/Storage/Impl.thy
     2     Author:     Olaf Müller
     2     Author:     Olaf Müller
     3 *)
     3 *)
     4 
     4 
     5 header {* The implementation of a memory *}
     5 section {* The implementation of a memory *}
     6 
     6 
     7 theory Impl
     7 theory Impl
     8 imports IOA Action
     8 imports IOA Action
     9 begin
     9 begin
    10 
    10