equal
deleted
inserted
replaced
|
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"; |