changeset 8010 | 69032a618aa9 |
parent 7998 | 3d0c34795831 |
child 9000 | c20d58286a51 |
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*)