src/HOL/Modelcheck/ROOT.ML
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 17272 c63e5220ed77
child 23556 c09cc406460b
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
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