Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2005-02-15 16:56:57 -0800 (Tue, 15 Feb 2005)
Revision: 6678
Log message:
Proved a new induction principle for lists (tail_induction) and proved all_list_wf using it
Changes | Path |
+8 -0 | metaprl/theories/itt/itt_list2.ml |
+17366 -18455 | metaprl/theories/itt/itt_list2.prla |