equal
deleted
inserted
replaced
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow & Konrad Slind |
3 Author: Tobias Nipkow & Konrad Slind |
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 This is the ROOT file for the meta theory of I/O-Automata. |
6 This is the ROOT file for the meta theory of I/O-Automata. |
7 |
|
8 |
7 |
9 @inproceedings{Nipkow-Slind-IOA, |
8 @inproceedings{Nipkow-Slind-IOA, |
10 author={Tobias Nipkow and Konrad Slind}, |
9 author={Tobias Nipkow and Konrad Slind}, |
11 title={{I/O} Automata in {Isabelle/HOL}}, |
10 title={{I/O} Automata in {Isabelle/HOL}}, |
12 booktitle={Proc.\ TYPES Workshop 1994}, |
11 booktitle={Proc.\ TYPES Workshop 1994}, |
22 title={Combining Model Checking and Deduction for {I/O}-Automata}, |
21 title={Combining Model Checking and Deduction for {I/O}-Automata}, |
23 booktitle={Proc.\ TACAS Workshop}, |
22 booktitle={Proc.\ TACAS Workshop}, |
24 organization={Aarhus University, BRICS report}, |
23 organization={Aarhus University, BRICS report}, |
25 year=1995} |
24 year=1995} |
26 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
25 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz |
27 |
|
28 Should be executed in the subdirectory HOL/IOA/NTP. |
|
29 *) |
26 *) |
30 |
27 |
31 use_thy "Solve"; |
28 use_thy "Solve"; |