# HG changeset patch
# User webertj
# Date 1164645350 -3600
# Node ID d24fb16e1a1dfc192869709e7d235d3230b24c10
# Parent  63278052bb72382835f3f138ffaf9e7523dc9632
outermost universal quantifiers are stripped

diff -r 63278052bb72 -r d24fb16e1a1d src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon Nov 27 17:13:10 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Mon Nov 27 17:35:50 2006 +0100
@@ -163,8 +163,7 @@
 oops
 
 lemma "\<forall>a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
-  refute  -- {* quantification causes an expansion of the formula; the
-                previous version with free variables is refuted much faster *}
+  refute
 oops
 
 text {* "Every reflexive and symmetric relation is transitive." *}