src/HOLCF/IOA/Storage/ROOT.ML
changeset 39119 7bfa17bcd5ee
parent 33615 261abc2e3155
equal deleted inserted replaced
39118:12f3788be67b 39119:7bfa17bcd5ee
     1 (*  Title:      HOLCF/IOA/Storage/ROOT.ML
     1 (*  Title:      HOLCF/IOA/Storage/ROOT.ML
     2     Author:     Olaf Mueller
     2     Author:     Olaf Mueller
     3 
     3 
     4 Memory storage case study.
     4 Memory storage case study.
     5 *)
     5 *)
     6 
       
     7 goals_limit := 1;
       
     8 
       
     9 use_thys ["Correctness"];
     6 use_thys ["Correctness"];