author | blanchet |
Fri, 30 Apr 2010 14:52:06 +0200 | |
changeset 36573 | badb32303d1e |
parent 36572 | ed99188882b1 |
child 36574 | 870dfa6d00ce |
--- 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))"