src/FOL/ROOT.ML

uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
more robust handling of "|" within index;

(*  Title:      FOL/ROOT.ML
    ID:         $Id$

First-Order Logic with Natural Deduction.
*)

use_thy "FOL";