src/HOL/HOLCF/IOA/Storage/ROOT.ML
changeset 40774 0437dbc127b3
parent 39119 7bfa17bcd5ee
child 42151 4da4fc77664b
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"];