Removal of monotonicity reasoning involving "lost" and the theorem
Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder
to prove when Notes is available.
intro Introduction to Isabelle
ref The Isabelle Reference Manual
system The Isabelle System Manual
logics Isabelle's Object-Logics
ind-defs (Co)Inductive Definitions in ZF
axclass Tutorial on Axiomatic Type Classes