src/HOL/Nominal/Examples/ROOT.ML

the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive

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