equal
deleted
inserted
replaced
|
1 (* Title: HOL/IOA/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 meta theory of I/O-Automata. |
|
7 |
|
8 |
|
9 @inproceedings{Nipkow-Slind-IOA, |
|
10 author={Tobias Nipkow and Konrad Slind}, |
|
11 title={{I/O} Automata in {Isabelle/HOL}}, |
|
12 booktitle={Proc.\ TYPES Workshop 1994}, |
|
13 publisher=Springer, |
|
14 series=LNCS, |
|
15 note={To appear}} |
|
16 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz |
|
17 |
|
18 and |
|
19 |
|
20 @inproceedings{Mueller-Nipkow, |
|
21 author={Olaf M\"uller and Tobias Nipkow}, |
|
22 title={Combining Model Checking and Deduction for {I/O}-Automata}, |
|
23 booktitle={Proc.\ TACAS Workshop}, |
|
24 organization={Aarhus University, BRICS report}, |
|
25 year=1995} |
|
26 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
|
27 |
|
28 Should be executed in the subdirectory HOL/IOA/NTP. |
|
29 *) |
|
30 |
|
31 use_thy "Solve"; |