equal
deleted
inserted
replaced
4 Copyright 2003-2004 |
4 Copyright 2003-2004 |
5 |
5 |
6 Basic setup and documentation for the 'refute' (and 'refute_params') command. |
6 Basic setup and documentation for the 'refute' (and 'refute_params') command. |
7 *) |
7 *) |
8 |
8 |
|
9 header {* Refute *} |
|
10 |
|
11 theory Refute = Map |
|
12 |
|
13 files "Tools/prop_logic.ML" |
|
14 "Tools/sat_solver.ML" |
|
15 "Tools/refute.ML" |
|
16 "Tools/refute_isar.ML": |
|
17 |
|
18 use "Tools/prop_logic.ML" |
|
19 use "Tools/sat_solver.ML" |
|
20 use "Tools/refute.ML" |
|
21 use "Tools/refute_isar.ML" |
|
22 |
|
23 setup Refute.setup |
|
24 |
|
25 text {* |
|
26 \small |
|
27 \begin{verbatim} |
9 (* ------------------------------------------------------------------------- *) |
28 (* ------------------------------------------------------------------------- *) |
10 (* REFUTE *) |
29 (* REFUTE *) |
11 (* *) |
30 (* *) |
12 (* We use a SAT solver to search for a (finite) model that refutes a given *) |
31 (* We use a SAT solver to search for a (finite) model that refutes a given *) |
13 (* HOL formula. *) |
32 (* HOL formula. *) |
81 (* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
100 (* HOL/Refute.thy This file: loads the ML files, basic setup, *) |
82 (* documentation *) |
101 (* documentation *) |
83 (* HOL/Main.thy Sets default parameters *) |
102 (* HOL/Main.thy Sets default parameters *) |
84 (* HOL/ex/RefuteExamples.thy Examples *) |
103 (* HOL/ex/RefuteExamples.thy Examples *) |
85 (* ------------------------------------------------------------------------- *) |
104 (* ------------------------------------------------------------------------- *) |
86 |
105 \end{verbatim} |
87 header {* Refute *} |
106 *} |
88 |
|
89 theory Refute = Map |
|
90 |
|
91 files "Tools/prop_logic.ML" |
|
92 "Tools/sat_solver.ML" |
|
93 "Tools/refute.ML" |
|
94 "Tools/refute_isar.ML": |
|
95 |
|
96 use "Tools/prop_logic.ML" |
|
97 use "Tools/sat_solver.ML" |
|
98 use "Tools/refute.ML" |
|
99 use "Tools/refute_isar.ML" |
|
100 |
|
101 setup Refute.setup |
|
102 |
107 |
103 end |
108 end |