| changeset 39128 | 93a7365fb4ee |
| parent 38798 | 89f273ab1d42 |
| child 39795 | 9e59b4c11039 |
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 22:57:21 2010 +0200 +++ b/doc-src/TutorialI/Sets/Examples.thy Fri Sep 03 23:54:48 2010 +0200 @@ -1,6 +1,6 @@ theory Examples imports Main Binomial begin -ML "eta_contract := false" +declare [[eta_contract = false]] ML "Pretty.margin_default := 64" text{*membership, intersection *}