changeset 49988 | ef811090e106 |
parent 49834 | b27bbb021df1 |
child 55395 | 4e79187f847e |
49987:25e333d2eccd | 49988:ef811090e106 |
---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Examples for the 'refute' command *} |
8 header {* Examples for the 'refute' command *} |
9 |
9 |
10 theory Refute_Examples |
10 theory Refute_Examples |
11 imports Main |
11 imports "~~/src/HOL/Library/Refute" |
12 begin |
12 begin |
13 |
13 |
14 refute_params [satsolver = "dpll"] |
14 refute_params [satsolver = "dpll"] |
15 |
15 |
16 lemma "P \<and> Q" |
16 lemma "P \<and> Q" |