src/HOL/Modelcheck/ROOT.ML

spy_analz_tac: Restored iffI to the list of rules used to break down
the subgoal

(*  Title:      HOL/Modelcheck/ROOT.ML
    ID:         $Id$
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    Copyright   1997  TU Muenchen

This is the ROOT file for the Eindhoven Modelchecker example
*)


use_thy"Example";