Quot/ROOT.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 08 Dec 2009 11:59:16 +0100
changeset 621 c10a46fa0de9
parent 604 0cf166548856
child 628 a11b9b757f89
permissions -rw-r--r--
Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.

quick_and_dirty := true;

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