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