src/HOL/Nominal/Examples/ROOT.ML
author berghofe
Fri, 22 Sep 2006 14:30:37 +0200
changeset 20679 c09af1bd255a
parent 19499 1a082c1257d7
child 21086 fe9f43a1e5bd
permissions -rw-r--r--
Added function all_paths (formerly find_paths).

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