| author | kleing | 
| Wed, 26 Mar 2008 12:12:52 +0100 | |
| changeset 26402 | 441ddf3b8f02 | 
| parent 4529 | 21034b090722 | 
| child 33615 | 261abc2e3155 | 
| permissions | -rw-r--r-- | 
| 3078 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 1 | (* Title: HOL/IOA/ROOT.ML | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 2 | ID: $Id$ | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 3 | Author: Tobias Nipkow & Konrad Slind | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 4 | Copyright 1994 TU Muenchen | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 5 | |
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 6 | This is the ROOT file for the meta theory of I/O-Automata. | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 7 | |
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 8 | @inproceedings{Nipkow-Slind-IOA,
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 9 | author={Tobias Nipkow and Konrad Slind},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 10 | title={{I/O} Automata in {Isabelle/HOL}},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 11 | booktitle={Proc.\ TYPES Workshop 1994},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 12 | publisher=Springer, | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 13 | series=LNCS, | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 14 | note={To appear}}
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 15 | ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 16 | |
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 17 | and | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 18 | |
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 19 | @inproceedings{Mueller-Nipkow,
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 20 | author={Olaf M\"uller and Tobias Nipkow},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 21 | title={Combining Model Checking and Deduction for {I/O}-Automata},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 22 | booktitle={Proc.\ TACAS Workshop},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 23 | organization={Aarhus University, BRICS report},
 | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 24 | year=1995} | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 25 | ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 26 | *) | 
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 27 | |
| 
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
 mueller parents: diff
changeset | 28 | use_thy "Solve"; |