| author | chaieb | 
| Fri, 27 Mar 2009 17:35:21 +0000 | |
| changeset 30748 | fe67d729a61c | 
| 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";  |