# HG changeset patch
# User wenzelm
# Date 1085167057 -7200
# Node ID c2bf21b5564e2f5cb3faca9474d85e49ccab0600
# Parent  fe9504ba63d503930fd64a7312d140718a76ad61
load ML files only once;

diff -r fe9504ba63d5 -r c2bf21b5564e src/HOL/Refute.thy
--- a/src/HOL/Refute.thy	Fri May 21 21:16:51 2004 +0200
+++ b/src/HOL/Refute.thy	Fri May 21 21:17:37 2004 +0200
@@ -15,11 +15,6 @@
       "Tools/refute.ML"
       "Tools/refute_isar.ML":
 
-use "Tools/prop_logic.ML"
-use "Tools/sat_solver.ML"
-use "Tools/refute.ML"
-use "Tools/refute_isar.ML"
-
 setup Refute.setup
 
 text {*