src/HOL/Complex/ex/ROOT.ML
changeset 24631 c7da302a0346
parent 24216 2e2d81b4f184
equal deleted inserted replaced
24630:351a308ab58d 24631:c7da302a0346
    18   "BigO_Complex",
    18   "BigO_Complex",
    19 
    19 
    20   "Arithmetic_Series_Complex",
    20   "Arithmetic_Series_Complex",
    21   "HarmonicSeries",
    21   "HarmonicSeries",
    22 
    22 
    23   "DenumRat"
    23   "DenumRat",
       
    24   
       
    25   "MIR",
       
    26   "ReflectedFerrack"
    24 ];
    27 ];
    25 
    28 
    26 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
       
    27 else use_thys ["MIR", "ReflectedFerrack"];
       
    28