Nominal-General/ROOT.ML
author Christian Urban <urbanc@in.tum.de>
Sun, 09 May 2010 11:37:19 +0100
changeset 2080 0532006ec7ec
parent 1774 c34347ec7ab3
permissions -rw-r--r--
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied


no_document use_thys
   ["Nominal2_Base",
    "Nominal2_Eqvt",
    "Nominal2_Atoms",
    "Nominal2_Supp",
    "Atoms"];