src/HOL/Algebra/ROOT.ML
changeset 13940 c67798653056
parent 13936 d3671b878828
child 13943 83d842ccd4aa
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Apr 30 18:31:38 2003 +0200
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Apr 30 18:32:06 2003 +0200
     1.3 @@ -6,8 +6,9 @@
     1.4  
     1.5  (* New development, based on explicit structures *)
     1.6  
     1.7 +no_document use_thy "FuncSet";
     1.8  use_thy "Sylow";		(* Groups *)
     1.9 -(* use_thy "UnivPoly"; *)	(* Rings and polynomials *)
    1.10 +use_thy "UnivPoly";		(* Rings and polynomials *)
    1.11  
    1.12  (* Old development, based on axiomatic type classes.
    1.13     Will be withdrawn in future. *)