src/HOL/Complex/ex/ROOT.ML
changeset 23301 4c7e6d295980
parent 23264 324622260d29
child 23454 c54975167be9
     1.1 --- a/src/HOL/Complex/ex/ROOT.ML	Sun Jun 10 10:23:42 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Sun Jun 10 21:06:59 2007 +0200
     1.3 @@ -22,5 +22,9 @@
     1.4  use_thy "DenumRat";
     1.5  
     1.6  use_thy "Ferrante_Rackoff_Ex";
     1.7 -use_thy "MIR";
     1.8 -use_thy "ReflectedFerrack";
     1.9 \ No newline at end of file
    1.10 +
    1.11 +if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    1.12 +else use_thy "MIR";
    1.13 +
    1.14 +if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    1.15 +else use_thy "ReflectedFerrack";