src/FOL/FOL.thy

Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.

FOL = IFOL +
rules
classical "(~P ==> P) ==> P"
end