src/HOL/Modelcheck/ROOT.ML
changeset 3210 e80db1660614
child 6465 4086e4f2edc4
equal deleted inserted replaced
3209:ccb55f3121d1 3210:e80db1660614
       
     1 (*  Title:      HOL/Modelcheck/ROOT.ML
       
     2     ID:         $Id$
       
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
       
     4     Copyright   1997  TU Muenchen
       
     5 
       
     6 This is the ROOT file for the Eindhoven Modelchecker example
       
     7 *)
       
     8 
       
     9 
       
    10 use_thy"Example";