src/FOLP/ROOT.ML
author bulwahn
Fri, 27 Jan 2012 10:31:30 +0100
changeset 46343 6d9535e52915
parent 33615 261abc2e3155
permissions -rw-r--r--
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck

(*  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"];