src/HOL/Refute.thy
changeset 14589 feae7b5fd425
parent 14463 ed09706ecc5d
child 14771 c2bf21b5564e
     1.1 --- a/src/HOL/Refute.thy	Fri Apr 16 12:09:31 2004 +0200
     1.2 +++ b/src/HOL/Refute.thy	Fri Apr 16 13:51:04 2004 +0200
     1.3 @@ -6,6 +6,25 @@
     1.4  Basic setup and documentation for the 'refute' (and 'refute_params') command.
     1.5  *)
     1.6  
     1.7 +header {* Refute *}
     1.8 +
     1.9 +theory Refute = Map
    1.10 +
    1.11 +files "Tools/prop_logic.ML"
    1.12 +      "Tools/sat_solver.ML"
    1.13 +      "Tools/refute.ML"
    1.14 +      "Tools/refute_isar.ML":
    1.15 +
    1.16 +use "Tools/prop_logic.ML"
    1.17 +use "Tools/sat_solver.ML"
    1.18 +use "Tools/refute.ML"
    1.19 +use "Tools/refute_isar.ML"
    1.20 +
    1.21 +setup Refute.setup
    1.22 +
    1.23 +text {*
    1.24 +\small
    1.25 +\begin{verbatim}
    1.26  (* ------------------------------------------------------------------------- *)
    1.27  (* REFUTE                                                                    *)
    1.28  (*                                                                           *)
    1.29 @@ -83,21 +102,7 @@
    1.30  (* HOL/Main.thy               Sets default parameters                        *)
    1.31  (* HOL/ex/RefuteExamples.thy  Examples                                       *)
    1.32  (* ------------------------------------------------------------------------- *)
    1.33 -
    1.34 -header {* Refute *}
    1.35 -
    1.36 -theory Refute = Map
    1.37 -
    1.38 -files "Tools/prop_logic.ML"
    1.39 -      "Tools/sat_solver.ML"
    1.40 -      "Tools/refute.ML"
    1.41 -      "Tools/refute_isar.ML":
    1.42 -
    1.43 -use "Tools/prop_logic.ML"
    1.44 -use "Tools/sat_solver.ML"
    1.45 -use "Tools/refute.ML"
    1.46 -use "Tools/refute_isar.ML"
    1.47 -
    1.48 -setup Refute.setup
    1.49 +\end{verbatim}
    1.50 +*}
    1.51  
    1.52  end