# HG changeset patch
# User blanchet
# Date 1272631926 -7200
# Node ID badb32303d1ea1a9a9358c744a52eaa4a1a15576
# Parent  ed99188882b13c6bd2087a659140d5cc698d3ebd
remove debugging code

diff -r ed99188882b1 -r badb32303d1e src/HOL/Metis_Examples/set.thy
--- a/src/HOL/Metis_Examples/set.thy	Fri Apr 30 14:00:47 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy	Fri Apr 30 14:52:06 2010 +0200
@@ -8,8 +8,6 @@
 imports Main
 begin
 
-sledgehammer_params [isar_proof, debug, overlord]
-
 lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
                (S(x,y) | ~S(y,z) | Q(Z,Z))  &
                (Q(X,y) | ~Q(y,Z) | S(X,X))"