| changeset 41413 | 64cd30d6b0b8 |
| parent 39795 | 9e59b4c11039 |
| child 48611 | b34ff75c23a7 |
--- 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"