src/FOLP/ROOT.ML
author blanchet
Wed, 01 Jun 2011 10:29:43 +0200
changeset 43132 44cd26bfc30c
parent 33615 261abc2e3155
permissions -rw-r--r--
ensured monomorphized facts have normalized zero var indexes, so that "find_var" doesn't fail later on

(*  Title:      FOLP/ROOT.ML
    Author:     Martin Coen, Cambridge University Computer Laboratory
    Copyright   1993  University of Cambridge

Modifed version of Lawrence Paulson's FOL that contains proof terms.

Presence of unknown proof term means that matching does not behave as expected.
*)

use_thys ["FOLP"];