src/HOLCF/IOA/Storage/ROOT.ML
changeset 40774 0437dbc127b3
parent 40773 6c12f5e24e34
child 40775 ed7a4eadb2f6
equal deleted inserted replaced
40773:6c12f5e24e34 40774:0437dbc127b3
     1 (*  Title:      HOLCF/IOA/Storage/ROOT.ML
       
     2     Author:     Olaf Mueller
       
     3 
       
     4 Memory storage case study.
       
     5 *)
       
     6 use_thys ["Correctness"];