(* 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";