--- a/src/HOL/Refute.thy Thu Sep 02 16:45:21 2010 +0200
+++ b/src/HOL/Refute.thy Thu Sep 02 17:12:16 2010 +0200
@@ -9,9 +9,7 @@
theory Refute
imports Hilbert_Choice List
-uses
- "Tools/refute.ML"
- "Tools/refute_isar.ML"
+uses "Tools/refute.ML"
begin
setup Refute.setup
@@ -92,16 +90,14 @@
(* ------------------------------------------------------------------------- *)
(* FILES *)
(* *)
-(* HOL/Tools/prop_logic.ML Propositional logic *)
-(* HOL/Tools/sat_solver.ML SAT solvers *)
-(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
-(* Boolean assignment -> HOL model *)
-(* HOL/Tools/refute_isar.ML Adds 'refute'/'refute_params' to Isabelle's *)
-(* syntax *)
-(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
-(* documentation *)
-(* HOL/SAT.thy Sets default parameters *)
-(* HOL/ex/RefuteExamples.thy Examples *)
+(* HOL/Tools/prop_logic.ML Propositional logic *)
+(* HOL/Tools/sat_solver.ML SAT solvers *)
+(* HOL/Tools/refute.ML Translation HOL -> propositional logic and *)
+(* Boolean assignment -> HOL model *)
+(* HOL/Refute.thy This file: loads the ML files, basic setup, *)
+(* documentation *)
+(* HOL/SAT.thy Sets default parameters *)
+(* HOL/ex/Refute_Examples.thy Examples *)
(* ------------------------------------------------------------------------- *)
\end{verbatim}
*}