doc-src/TutorialI/Sets/Examples.thy
changeset 21262 a2bd14226f9a
parent 16417 9bc16273c2d4
child 32833 f3716d1a2e48
equal deleted inserted replaced
21261:58223c67fd8b 21262:a2bd14226f9a
     1 (* ID:         $Id$ *)
     1 (* ID:         $Id$ *)
     2 theory Examples imports Main begin
     2 theory Examples imports Main Binomial begin
     3 
     3 
     4 ML "reset eta_contract"
     4 ML "reset eta_contract"
     5 ML "Pretty.setmargin 64"
     5 ML "Pretty.setmargin 64"
     6 
     6 
     7 text{*membership, intersection *}
     7 text{*membership, intersection *}