simultaneous use_thys;
authorwenzelm
Fri Aug 10 15:28:11 2007 +0200 (2007-08-10)
changeset 242162e2d81b4f184
parent 24215 5458fbf18276
child 24217 5c4913b478f5
simultaneous use_thys;
src/HOL/Complex/ex/ROOT.ML
     1.1 --- a/src/HOL/Complex/ex/ROOT.ML	Fri Aug 10 15:13:18 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/ROOT.ML	Fri Aug 10 15:28:11 2007 +0200
     1.3 @@ -1,28 +1,28 @@
     1.4  (*  Title:      HOL/Complex/ex/ROOT.ML
     1.5      ID:         $Id$
     1.6  
     1.7 -Miscellaneous examples involving the Reals, Hyperreals, etc.
     1.8 +Miscellaneous examples.
     1.9  *)
    1.10  
    1.11 -use_thy "BinEx";
    1.12 -no_document (with_path "../../NumberTheory" use_thy) "Factorization";
    1.13 -(*These two examples just need the theory Primes.*)
    1.14 -use_thy "Sqrt";
    1.15 -use_thy "Sqrt_Script";
    1.16 -(*This example also needs the theory Factorization.*)
    1.17 -use_thy "NSPrimes";
    1.18 +no_document use_thys [
    1.19 +  "../../NumberTheory/Factorization",
    1.20 +  "BigO",
    1.21 +  "NatPair"
    1.22 +];
    1.23  
    1.24 -no_document use_thy "BigO";
    1.25 -use_thy "BigO_Complex";
    1.26 +use_thys [
    1.27 +  "BinEx",
    1.28 +  "Sqrt",
    1.29 +  "Sqrt_Script",
    1.30 +  "NSPrimes",
    1.31 +  "BigO_Complex",
    1.32  
    1.33 -use_thy "Arithmetic_Series_Complex";
    1.34 -use_thy "HarmonicSeries";
    1.35 +  "Arithmetic_Series_Complex",
    1.36 +  "HarmonicSeries",
    1.37  
    1.38 -no_document use_thy "NatPair";
    1.39 -use_thy "DenumRat";
    1.40 +  "DenumRat"
    1.41 +];
    1.42  
    1.43  if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    1.44 -else use_thy "MIR";
    1.45 +else use_thys ["MIR", "ReflectedFerrack"];
    1.46  
    1.47 -if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    1.48 -else use_thy "ReflectedFerrack";