accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
Context.theory_name;
(* Title: FOLP/FOLP.thy
ID: $Id$
Author: Martin D Coen, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Classical First-Order Logic with Proofs
*)
FOLP = IFOLP +
consts
cla :: "[p=>p]=>p"
rules
classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
end