changeset 66453 | cc19f7ca2ed6 |
parent 63901 | 4ce989e962e0 |
child 67399 | eab6ce8368fa |
66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
---|---|
6 *) |
6 *) |
7 |
7 |
8 section \<open>Examples for the 'refute' command\<close> |
8 section \<open>Examples for the 'refute' command\<close> |
9 |
9 |
10 theory Refute_Examples |
10 theory Refute_Examples |
11 imports "~~/src/HOL/Library/Refute" |
11 imports "HOL-Library.Refute" |
12 begin |
12 begin |
13 |
13 |
14 refute_params [satsolver = "cdclite"] |
14 refute_params [satsolver = "cdclite"] |
15 |
15 |
16 lemma "P \<and> Q" |
16 lemma "P \<and> Q" |