# HG changeset patch # User krauss # Date 1165241759 -3600 # Node ID 32f3e1127de2773ba0b6410211b8103d92cde594 # Parent 369e38e3568668295616f1298c0ecc785f1d3f7f added Ramsey.thy to Library imports, to include it in the daily builds diff -r 369e38e35686 -r 32f3e1127de2 src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Mon Dec 04 15:15:09 2006 +0100 +++ b/src/HOL/Library/Library.thy Mon Dec 04 15:15:59 2006 +0100 @@ -25,6 +25,7 @@ Permutation Primes Quotient + Ramsey State_Monad While_Combinator Word