| author | blanchet |
| Mon, 22 Aug 2011 15:02:45 +0200 | |
| changeset 44401 | c47f118fe008 |
| parent 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 |
Author: Tobias Nipkow & Konrad Slind |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Copyright 1994 TU Muenchen |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
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
|
6 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
7 |
@inproceedings{Nipkow-Slind-IOA,
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
8 |
author={Tobias Nipkow and Konrad Slind},
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
9 |
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
|
10 |
booktitle={Proc.\ TYPES Workshop 1994},
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
publisher=Springer, |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
12 |
series=LNCS, |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
13 |
note={To appear}}
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
14 |
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
|
15 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
16 |
and |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
17 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
18 |
@inproceedings{Mueller-Nipkow,
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
booktitle={Proc.\ TACAS Workshop},
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
22 |
organization={Aarhus University, BRICS report},
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
23 |
year=1995} |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
24 |
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
|
25 |
*) |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
26 |
|
| 33615 | 27 |
use_thys ["Solve"]; |