src/HOL/Modelcheck/ROOT.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 23556 c09cc406460b
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
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@17272
     8
time_use_thy "CTL";
wenzelm@17272
     9
wenzelm@17272
    10
wenzelm@17272
    11
(* Einhoven model checker *)
wenzelm@17272
    12
wenzelm@17272
    13
time_use_thy "EindhovenSyn";
wenzelm@17272
    14
if_eindhoven_enabled time_use_thy "EindhovenExample";
wenzelm@17272
    15
wenzelm@7295
    16
wenzelm@7295
    17
(* Mucke -- mu-calculus model checker from Karlsruhe *)
wenzelm@7295
    18
wenzelm@9000
    19
time_use "mucke_oracle.ML";
wenzelm@9000
    20
time_use_thy "MuckeSyn";
mueller@3210
    21
wenzelm@9000
    22
if_mucke_enabled time_use_thy "MuckeExample1";
wenzelm@9000
    23
if_mucke_enabled time_use_thy "MuckeExample2";
wenzelm@7295
    24
wenzelm@7295
    25