src/HOL/Nominal/ROOT.ML
author paulson
Fri, 02 Mar 2007 12:37:34 +0100
changeset 22382 dbf09db0a40d
parent 20809 6c4fd0b4b63a
child 24584 01e83ffa6c54
permissions -rw-r--r--
New code to store theorem names in a concise form rather than as fully-qualified. Meson.is_fol_term now takes a theory as argument.

(*  Title:      HOL/Nominal/nominal_atoms.ML
    ID:         $Id$
    Author:     Stefan Berghofer and Christian Urban, TU Muenchen

The nominal datatype package.
*)

no_document use_thy "Infinite_Set";
use_thy "Nominal";