Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting
(* 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