added none: 'a -> 'a * 'b attribute list;
added no_attrs: 'a * 'b -> ('a * ('b * tag list)) * 'c attribute list;
added no_attrss: 'a * 'b list -> ('a * ('b * tag list) list) * 'c attribute list;
added applys: ('a * tthm list) * 'a attribute list -> ('a * tthm list);
(* 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