Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-17 19:58:16 -0700 (Tue, 17 Jun 2003)
Revision: 4671
Log message:

      Added (during the last CS101 lecture) a "smallest_element" theorem
      that establishes an existence of the smallest element in any list.
      This can be used to demo the extractor (once it actually works).
      

Changes	Path
+11 -0	metaprl/theories/itt/itt_sort.ml
+3417 -2942	metaprl/theories/itt/itt_sort.prla