
diff -r 35f30e07fe0d -r 64cd30d6b0b8 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 13:51:17 2010 +0100
+++ b/doc-src/TutorialI/Sets/Examples.thy	Wed Dec 29 17:34:41 2010 +0100
@@ -1,4 +1,4 @@
-theory Examples imports Main Binomial begin
+theory Examples imports Main "~~/src/HOL/Library/Binomial" begin
 
 declare [[eta_contract = false]]
 ML "Pretty.margin_default := 64"




