use was wrong...
authorchaieb
Wed, 14 Sep 2005 21:35:46 +0200
changeset 17380 8d143599daa9
parent 17379 85109eec887b
child 17381 ec9997d0a3ff
use was wrong...
src/HOL/Commutative_Ring.thy
--- a/src/HOL/Commutative_Ring.thy	Wed Sep 14 19:03:16 2005 +0200
+++ b/src/HOL/Commutative_Ring.thy	Wed Sep 14 21:35:46 2005 +0200
@@ -7,7 +7,7 @@
 
 theory Commutative_Ring
 imports List
-uses ("comm_ring.ML")
+uses ("Tools/comm_ring.ML")
 begin
 
   (* Syntax of multivariate polynomials (pol) and polynomial expressions*)
@@ -304,7 +304,7 @@
 generate_code ("ring.ML") test = "norm"*)
 
 
- use "comm_ring.ML"
+ use "Tools/comm_ring.ML"
 setup "CommRing.setup"
 
-end
\ No newline at end of file
+end