src/HOL/Nominal/Examples/ROOT.ML

declare fps_nth as a typedef morphism; clean up instance proofs

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

setmp_noncritical quick_and_dirty true use_thy "VC_Condition";