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
mueller@3210
     1
(*  Title:      HOL/Modelcheck/ROOT.ML
mueller@3210
     2
    ID:         $Id$
wenzelm@7295
     3
    Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
mueller@3210
     4
wenzelm@7295
     5
Basic Modelchecker examples.
mueller@3210
     6
*)
mueller@3210
     7
wenzelm@7295
     8
wenzelm@7295
     9
(* Mucke -- mu-calculus model checker from Karlsruhe *)
wenzelm@7295
    10
wenzelm@9000
    11
time_use "mucke_oracle.ML";
wenzelm@9000
    12
time_use_thy "MuckeSyn";
mueller@3210
    13
wenzelm@9000
    14
if_mucke_enabled time_use_thy "MuckeExample1";
wenzelm@9000
    15
if_mucke_enabled time_use_thy "MuckeExample2";
wenzelm@7295
    16
wenzelm@7295
    17
wenzelm@7295
    18
(* Einhoven model checker *)
wenzelm@7295
    19
wenzelm@9000
    20
time_use_thy "CTL";
wenzelm@9000
    21
time_use_thy "EindhovenSyn";
wenzelm@7295
    22
wenzelm@9000
    23
if_eindhoven_enabled time_use_thy "EindhovenExample";