src/HOL/Nominal/Examples/ROOT.ML

deleted card definition as code lemma; authentic syntax for card

(*  Title:      HOL/Nominal/Examples/ROOT.ML
    ID:         $Id$
    Author:     Christian Urban, TU Muenchen

Various examples involving nominal datatypes.
*)

use_thys [
  "CR",
  "CR_Takahashi",
  "Class",
  "Compile",
  "Fsub",
  "Height",
  "Lambda_mu",
  "SN",
  "Weakening",
  "Crary",
  "SOS",
  "LocalWeakening",
  "Support"
];

setmp quick_and_dirty true use_thy "VC_Compatible";