src/HOL/Algebra/ROOT.ML
changeset 24153 1a4607b7ad24
parent 21256 47195501ecf7
child 27713 95b36bfe7fc4
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Fri Aug 03 22:35:40 2007 +0200
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Fri Aug 03 22:50:40 2007 +0200
     1.3 @@ -4,29 +4,28 @@
     1.4      Author: Clemens Ballarin, started 24 September 1999
     1.5  *)
     1.6  
     1.7 -(*** New development, based on explicit structures ***)
     1.8 -
     1.9  (* Preliminaries from set and number theory *)
    1.10 -
    1.11 -no_document use_thy "FuncSet";
    1.12 -no_document use_thy "Primes";
    1.13 -no_document use_thy "Binomial";
    1.14 +no_document use_thys ["FuncSet", "Primes", "Binomial"];
    1.15  
    1.16  
    1.17 -(* Groups *)
    1.18 +(*** New development, based on explicit structures ***)
    1.19  
    1.20 -use_thy "FiniteProduct";	(* Product operator for commutative groups *)
    1.21 -use_thy "Sylow";		(* Sylow's theorem *)
    1.22 -use_thy "Bij";			(* Automorphism Groups *)
    1.23 +use_thys [
    1.24 +  (* Groups *)
    1.25 +  "FiniteProduct",      (* Product operator for commutative groups *)
    1.26 +  "Sylow",              (* Sylow's theorem *)
    1.27 +  "Bij",                (* Automorphism Groups *)
    1.28  
    1.29 -(* Rings *)
    1.30 -
    1.31 -use_thy "UnivPoly";		(* Rings and polynomials *)
    1.32 -use_thy "IntRing";		(* Ideals and residue classes *)
    1.33 +  (* Rings *)
    1.34 +  "UnivPoly",           (* Rings and polynomials *)
    1.35 +  "IntRing"             (* Ideals and residue classes *)
    1.36 +];
    1.37  
    1.38  
    1.39  (*** Old development, based on axiomatic type classes.
    1.40       Will be withdrawn in future. ***)
    1.41  
    1.42 -with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
    1.43 -with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)
    1.44 +no_document use_thys [
    1.45 +  "abstract/Abstract",  (*The ring theory*)
    1.46 +  "poly/Polynomial"     (*The full theory*)
    1.47 +];