Nominal/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Wed, 07 Apr 2010 17:37:29 +0200
changeset 1778 88ec05a09772
parent 1774 c34347ec7ab3
child 1795 e39453c8b186
permissions -rw-r--r--
added an induction principle for permutations; removed add_perm construction

quick_and_dirty := true;

no_document use_thys
   ["Ex/ExLam",
    "Ex/ExLF",
    "Ex/Ex1",
    "Ex/Ex1rec",
    "Ex/Ex2",
    "Ex/Ex3",
    "Ex/ExLet",
    "Ex/ExLetRec",
    "Ex/ExTySch",
    "Ex/ExLeroy",
    "Ex/ExPS3",
    "Ex/ExPS7",
    "Ex/ExCoreHaskell",
    "Ex/Test"
(*  "Ex/ExPS6", *)
    ];