1355
|
1 |
(* Title: HOL/IOA/NTP/ROOT.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
4 |
Copyright 1994 TU Muenchen
|
|
5 |
|
|
6 |
This is the ROOT file for the theory of I/O-Automata (NTP subdirectory).
|
|
7 |
The formalization is by a semantic model of I/O-Automata.
|
|
8 |
For details see
|
|
9 |
|
|
10 |
@inproceedings{Nipkow-Slind-IOA,
|
|
11 |
author={Tobias Nipkow and Konrad Slind},
|
|
12 |
title={{I/O} Automata in {Isabelle/HOL}},
|
|
13 |
booktitle={Proc.\ TYPES Workshop 1994},
|
|
14 |
publisher=Springer,
|
|
15 |
series=LNCS,
|
|
16 |
note={To appear}}
|
|
17 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
|
|
18 |
|
|
19 |
and
|
|
20 |
|
|
21 |
@inproceedings{Mueller-Nipkow,
|
|
22 |
author={Olaf M\"uller and Tobias Nipkow},
|
|
23 |
title={Combining Model Checking and Deduction for {I/O}-Automata},
|
|
24 |
booktitle={Proc.\ TACAS Workshop},
|
|
25 |
organization={Aarhus University, BRICS report},
|
|
26 |
year=1995}
|
|
27 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
|
|
28 |
|
|
29 |
Should be executed in the subdirectory HOL/IOA/NTP.
|
|
30 |
*)
|
|
31 |
|
|
32 |
goals_limit := 1;
|
|
33 |
|
|
34 |
loadpath := [".", "../meta_theory"];
|
|
35 |
use_thy "Correctness";
|