src/HOL/Complex/ex/ROOT.ML
changeset 23301 4c7e6d295980
parent 23264 324622260d29
child 23454 c54975167be9
equal deleted inserted replaced
23300:b785068bd5dc 23301:4c7e6d295980
    20 
    20 
    21 no_document use_thy "NatPair";
    21 no_document use_thy "NatPair";
    22 use_thy "DenumRat";
    22 use_thy "DenumRat";
    23 
    23 
    24 use_thy "Ferrante_Rackoff_Ex";
    24 use_thy "Ferrante_Rackoff_Ex";
    25 use_thy "MIR";
    25 
    26 use_thy "ReflectedFerrack";
    26 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
       
    27 else use_thy "MIR";
       
    28 
       
    29 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
       
    30 else use_thy "ReflectedFerrack";