src/HOL/Nominal/Examples/ROOT.ML

avoid duplicate fact bindings;

(*  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",
  "Contexts" 
];

setmp quick_and_dirty true use_thy "VC_Condition";