added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
(* 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";