spy_analz_tac: Restored iffI to the list of rules used to break down
the subgoal
intro Introduction to Isabelleref The Isabelle Reference Manualsystem The Isabelle System Manuallogics Isabelle's Object-Logicsind-defs (Co)Inductive Definitions in ZFaxclass Tutorial on Axiomatic Type Classes