src/HOL/IOA/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/ROOT.ML	Wed Apr 30 11:56:17 1997 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/IOA/ROOT.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+This is the ROOT file for the meta theory of I/O-Automata.
+
+
+@inproceedings{Nipkow-Slind-IOA,
+author={Tobias Nipkow and Konrad Slind},
+title={{I/O} Automata in {Isabelle/HOL}},
+booktitle={Proc.\ TYPES Workshop 1994},
+publisher=Springer,
+series=LNCS,
+note={To appear}}
+ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
+
+and
+
+@inproceedings{Mueller-Nipkow,
+author={Olaf M\"uller and Tobias Nipkow},
+title={Combining Model Checking and Deduction for {I/O}-Automata},
+booktitle={Proc.\ TACAS Workshop},
+organization={Aarhus University, BRICS report},
+year=1995}
+ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
+
+Should be executed in the subdirectory HOL/IOA/NTP.
+*)
+
+use_thy "Solve";