Quot/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Mon, 07 Dec 2009 21:53:50 +0100
changeset 610 2bee5ca44ef5
parent 604 0cf166548856
child 628 a11b9b757f89
permissions -rw-r--r--
removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>

quick_and_dirty := true;

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