equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Alwen Tiu, Tjark Weber |
3 Author: Alwen Tiu, Tjark Weber |
4 Copyright 2005 |
4 Copyright 2005 |
5 *) |
5 *) |
6 |
6 |
7 header {* Examples for the 'sat' command *} |
7 header {* Examples for the 'sat' and 'satx' tactic *} |
8 |
8 |
9 theory SAT_Examples imports Main |
9 theory SAT_Examples imports Main |
10 |
10 |
11 begin |
11 begin |
|
12 |
|
13 ML {* set sat.trace_sat; *} |
12 |
14 |
13 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *) |
15 (* Translated from TPTP problem library: PUZ015-2.006.dimacs *) |
14 |
16 |
15 lemma assumes 1: "~x0" |
17 lemma assumes 1: "~x0" |
16 and 2: "~x30" |
18 and 2: "~x30" |