author | wenzelm |
Thu, 11 Nov 1999 11:58:51 +0100 | |
changeset 8010 | 69032a618aa9 |
parent 8009 | 29a7a79ee7f4 |
child 8011 | d14c4e9e9c8e |
1.1 --- a/src/HOL/Algebra/ROOT.ML Thu Nov 11 11:43:14 1999 +0100 1.2 +++ b/src/HOL/Algebra/ROOT.ML Thu Nov 11 11:58:51 1999 +0100 1.3 @@ -4,8 +4,5 @@ 1.4 Author: Clemens Ballarin, started 24 September 1999 1.5 *) 1.6 1.7 -add_path "abstract"; 1.8 -add_path "poly"; 1.9 - 1.10 -use_thy "Abstract"; (*The ring theory*) 1.11 -use_thy "Polynomial"; (*The full theory*) 1.12 +with_path "abstract" use_thy "Abstract"; (*The ring theory*) 1.13 +with_path "poly" use_thy "Polynomial"; (*The full theory*)