src/HOL/UNITY/ROOT.ML
changeset 28529 7ff939586e83
parent 24147 edc90be09ac1
child 28866 30cd9d89a0fb
equal deleted inserted replaced
28528:0cf2749e8ef7 28529:7ff939586e83
    41   "ELT"
    41   "ELT"
    42 ];
    42 ];
    43 
    43 
    44 (*Allocator example*)
    44 (*Allocator example*)
    45 (* FIXME some parts no longer work -- had been commented out for a long time *)
    45 (* FIXME some parts no longer work -- had been commented out for a long time *)
    46 setmp quick_and_dirty true
    46 setmp_noncritical quick_and_dirty true
    47   use_thy "Comp/Alloc";
    47   use_thy "Comp/Alloc";
    48 
    48 
    49 use_thys ["Comp/AllocImpl", "Comp/Client"];
    49 use_thys ["Comp/AllocImpl", "Comp/Client"];