Quot/ROOT.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 08 Dec 2009 13:08:56 +0100
changeset 626 28e9c770a082
parent 604 0cf166548856
child 628 a11b9b757f89
permissions -rw-r--r--
Finished the proof of ttt2 and found bug in regularize when trying ttt3.

quick_and_dirty := true;

no_document use_thys
   ["QuotMain",
    "Examples/Fset",
    "Examples/IntEx",
    "Examples/IntEx2",
    "Examples/LFex",
    "Examples/LamEx"];