# HG changeset patch
# User wenzelm
# Date 1163069927 -3600
# Node ID a2bd14226f9a1898c779df5883c1c6a35ce031f5
# Parent  58223c67fd8b12724b3fdd3f69b1ee285728c3aa
imports Binimial;

diff -r 58223c67fd8b -r a2bd14226f9a doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Nov 09 11:58:45 2006 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Nov 09 11:58:47 2006 +0100
@@ -1,5 +1,5 @@
 (* ID:         $Id$ *)
-theory Examples imports Main begin
+theory Examples imports Main Binomial begin
 
 ML "reset eta_contract"
 ML "Pretty.setmargin 64"