| changeset 59667 | 651ea265d568 |
| parent 55159 | 608c157d743d |
| child 67406 | 23307fd33906 |
--- a/src/Doc/Tutorial/Sets/Examples.thy Tue Mar 10 11:56:32 2015 +0100 +++ b/src/Doc/Tutorial/Sets/Examples.thy Tue Mar 10 15:20:40 2015 +0000 @@ -1,4 +1,4 @@ -theory Examples imports "~~/src/HOL/Number_Theory/Binomial" begin +theory Examples imports Complex_Main begin declare [[eta_contract = false]]