(* Title: HOL/Nominal/Examples/ROOT.ML ID: $Id$ Author: Christian Urban, TU Muenchen Various examples involving nominal datatypes. *) use_thy "CR"; use_thy "Class"; setmp quick_and_dirty true use_thy "Fsub"; (* FIXME *) use_thy "Lambda_mu"; use_thy "Recursion"; use_thy "SN"; use_thy "Weakening";