doc-src/TutorialI/Sets/Examples.thy
changeset 38798 89f273ab1d42
parent 36745 403585a89772
child 39128 93a7365fb4ee
--- a/doc-src/TutorialI/Sets/Examples.thy	Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Fri Aug 27 14:07:09 2010 +0200
@@ -1,7 +1,6 @@
-(* ID:         $Id$ *)
 theory Examples imports Main Binomial begin
 
-ML "Unsynchronized.reset eta_contract"
+ML "eta_contract := false"
 ML "Pretty.margin_default := 64"
 
 text{*membership, intersection *}