# HG changeset patch
# User webertj
# Date 1138303074 -3600
# Node ID 8a5c6fc3ad27aff41d3930cc06892573a0bdcd00
# Parent  4f4ed2a01152af2656d3368f1a904be9668456aa
smaller example to prevent timeout

diff -r 4f4ed2a01152 -r 8a5c6fc3ad27 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Jan 26 17:58:01 2006 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Jan 26 20:17:54 2006 +0100
@@ -156,13 +156,13 @@
   apply fast
 done
 
-text {* "A type has at most 5 elements." *}
+text {* "A type has at most 4 elements." *}
 
-lemma "a=b | a=c | a=d | a=e | a=f | b=c | b=d | b=e | b=f | c=d | c=e | c=f | d=e | d=f | e=f"
+lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
   refute
 oops
 
-lemma "\<forall>a b c d e f. a=b | a=c | a=d | a=e | a=f | b=c | b=d | b=e | b=f | c=d | c=e | c=f | d=e | d=f | e=f"
+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 *}
 oops