src/FOL/ROOT.ML
author huffman
Fri, 24 Feb 2012 16:53:59 +0100
changeset 46653 a557db8f2fbf
parent 33615 261abc2e3155
permissions -rw-r--r--
avoid using BIT_simps in proofs; rephrase lemmas without Int.succ or Int.pred;

(* First-Order Logic with Natural Deduction *)

use_thys ["FOL"];