# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID ef811090e1062cd1c381c19b772c5f0d1a8a08d0
# Parent  25e333d2eccd095e083215b4437896ffd0a0adab
fixes related to Refute's move

diff -r 25e333d2eccd -r ef811090e106 src/HOL/ex/Refute_Examples.thy
--- 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"]