src/HOL/Nominal/Examples/ROOT.ML
author urbanc
Tue, 16 Jan 2007 13:59:08 +0100
changeset 22073 c170dcbe6c9d
parent 21136 85fd05aaf737
child 22448 f982e73e36de
permissions -rw-r--r--
formalisation of Crary's chapter on logical relations (in the book on Advanced Topics in Type Systems) done by Narboux and Urban

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

Various examples involving nominal datatypes.
*)

use_thy "CR";
use_thy "Class";
use_thy "Compile";
use_thy "Fsub";
use_thy "Height";
use_thy "Lambda_mu";
use_thy "SN";
use_thy "Weakening";
use_thy "Crary";