src/HOL/Nominal/Examples/ROOT.ML

basic setup for generated document sources (cf. IsarRef/isar-ref.tex);

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

setmp quick_and_dirty true use_thy "VC_Condition";