| changeset 49988 | ef811090e106 |
| parent 49834 | b27bbb021df1 |
| child 55395 | 4e79187f847e |
--- a/src/HOL/ex/Refute_Examples.thy Wed Oct 31 11:23:21 2012 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Wed Oct 31 11:23:21 2012 +0100 @@ -8,7 +8,7 @@ header {* Examples for the 'refute' command *} theory Refute_Examples -imports Main +imports "~~/src/HOL/Library/Refute" begin refute_params [satsolver = "dpll"]