Nominal/ROOT.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 29 Mar 2010 18:12:54 +0200
changeset 1701 58abc09d6f9c
parent 1656 c9d3dda79fe3
child 1773 c0eac04ae3b4
permissions -rw-r--r--
Updated strong induction to modified definitions.

quick_and_dirty := true;

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