equal
deleted
inserted
replaced
1 (* Title: HOL/Modelcheck/ROOT.ML |
1 (* Title: HOL/Modelcheck/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Mueller, Tobias Hamberger, Robert Sandner |
3 Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen |
4 Copyright 1997 TU Muenchen |
|
5 |
4 |
6 This is the ROOT file for the Modelchecker examples |
5 Basic Modelchecker examples. |
7 *) |
6 *) |
8 |
7 |
9 use_thy"EindhovenExample"; |
|
10 |
8 |
11 use"mucke_oracle.ML"; |
9 (* Mucke -- mu-calculus model checker from Karlsruhe *) |
12 use_thy"MuckeExample1"; |
10 |
13 use_thy"MuckeExample2"; |
11 use "mucke_oracle.ML"; |
|
12 use_thy "MuckeSyn"; |
|
13 |
|
14 if_mucke_enabled use_thy "MuckeExample1"; |
|
15 if_mucke_enabled use_thy "MuckeExample2"; |
|
16 |
|
17 |
|
18 (* Einhoven model checker *) |
|
19 |
|
20 use_thy "CTL"; |
|
21 use_thy "EindhovenSyn"; |
|
22 |
|
23 if_eindhoven_enabled use_thy "EindhovenExample"; |