src/HOLCF/HOLCF.thy
changeset 23152 9497234a2743
parent 19105 3aabd46340e0
child 25904 8161f137b0e9
--- a/src/HOLCF/HOLCF.thy	Thu May 31 13:24:13 2007 +0200
+++ b/src/HOLCF/HOLCF.thy	Thu May 31 14:01:58 2007 +0200
@@ -9,13 +9,13 @@
 imports Sprod Ssum Up Lift Discrete One Tr Domain Main
 uses
   "holcf_logic.ML"
-  "cont_consts.ML"
-  "domain/library.ML"
-  "domain/syntax.ML"
-  "domain/axioms.ML"
-  "domain/theorems.ML"
-  "domain/extender.ML"
-  "adm_tac.ML"
+  "Tools/cont_consts.ML"
+  "Tools/domain/domain_library.ML"
+  "Tools/domain/domain_syntax.ML"
+  "Tools/domain/domain_axioms.ML"
+  "Tools/domain/domain_theorems.ML"
+  "Tools/domain/domain_extender.ML"
+  "Tools/adm_tac.ML"
 
 begin