src/HOL/Modelcheck/ROOT.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 9000 c20d58286a51
child 17272 c63e5220ed77
permissions -rw-r--r--
Constant "If" is now local
     1 (*  Title:      HOL/Modelcheck/ROOT.ML
     2     ID:         $Id$
     3     Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
     4 
     5 Basic Modelchecker examples.
     6 *)
     7 
     8 
     9 (* Mucke -- mu-calculus model checker from Karlsruhe *)
    10 
    11 time_use "mucke_oracle.ML";
    12 time_use_thy "MuckeSyn";
    13 
    14 if_mucke_enabled time_use_thy "MuckeExample1";
    15 if_mucke_enabled time_use_thy "MuckeExample2";
    16 
    17 
    18 (* Einhoven model checker *)
    19 
    20 time_use_thy "CTL";
    21 time_use_thy "EindhovenSyn";
    22 
    23 if_eindhoven_enabled time_use_thy "EindhovenExample";