doc-src/TutorialI/Sets/Examples.thy
changeset 32833 f3716d1a2e48
parent 21262 a2bd14226f9a
child 35416 d8d7d1b785af
equal deleted inserted replaced
32827:2729c8033326 32833:f3716d1a2e48
     1 (* ID:         $Id$ *)
     1 (* ID:         $Id$ *)
     2 theory Examples imports Main Binomial begin
     2 theory Examples imports Main Binomial begin
     3 
     3 
     4 ML "reset eta_contract"
     4 ML "Unsynchronized.reset eta_contract"
     5 ML "Pretty.setmargin 64"
     5 ML "Pretty.setmargin 64"
     6 
     6 
     7 text{*membership, intersection *}
     7 text{*membership, intersection *}
     8 text{*difference and empty set*}
     8 text{*difference and empty set*}
     9 text{*complement, union and universal set*}
     9 text{*complement, union and universal set*}