src/FOL/ROOT.ML

It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...

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

First-Order Logic with Natural Deduction.
*)

use_thy "FOL";