| author | mueller |
| Thu, 22 Apr 1999 11:09:05 +0200 | |
| changeset 6471 | 08d12ef5fc19 |
| child 6488 | 271969bb7f95 |
| permissions | -rw-r--r-- |
|
6471
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/IOA/Modelcheck/ROOT.ML |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
3 |
Author: Olaf Mueller |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
4 |
Copyright 1997 TU Muenchen |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
5 |
|
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
6 |
This is the ROOT file for the formalization of a semantic model of |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
7 |
I/O-Automata. See the README.html file for details. |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
8 |
*) |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
9 |
|
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
10 |
goals_limit := 1; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
11 |
|
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
12 |
add_path"~/isabelle/src/HOL/Modelcheck"; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
13 |
use"~/isabelle/src/HOL/Modelcheck/mucke_oracle.ML"; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
14 |
use_thy"MuIOAOracle"; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
15 |
use_thy"Cockpit"; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
16 |
use_thy"Ring3"; |
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
17 |
|
|
08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller
parents:
diff
changeset
|
18 |
reset_path(); |