src/HOL/Nominal/Examples/ROOT.ML
author wenzelm
Sun, 08 Jun 2008 14:29:09 +0200
changeset 27090 2f45c1b1b05d
parent 25722 0a104ddb72d9
child 27623 8e9c19529a4e
permissions -rw-r--r--
remove codegen_process.pdf from distribution;

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