src/HOL/IOA/ABP/ROOT.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 1354 39506f728115
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@1354
     1
(*  Title:      HOL/IOA/ABP/ROOT.ML
clasohm@1354
     2
    ID:         $Id$
clasohm@1354
     3
    Author:     Tobias Nipkow & Konrad Slind
clasohm@1354
     4
    Copyright   1994  TU Muenchen
clasohm@1354
     5
clasohm@1354
     6
This is the ROOT file for the theory of I/O-Automata (ABP subdirectory).
clasohm@1354
     7
The formalization is by a semantic model of I/O-Automata.
clasohm@1354
     8
For details see
clasohm@1354
     9
clasohm@1354
    10
@inproceedings{Nipkow-Slind-IOA,
clasohm@1354
    11
author={Tobias Nipkow and Konrad Slind},
clasohm@1354
    12
title={{I/O} Automata in {Isabelle/HOL}},
clasohm@1354
    13
booktitle={Proc.\ TYPES Workshop 1994},
clasohm@1354
    14
publisher=Springer,
clasohm@1354
    15
series=LNCS,
clasohm@1354
    16
note={To appear}}
clasohm@1354
    17
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
clasohm@1354
    18
clasohm@1354
    19
and
clasohm@1354
    20
clasohm@1354
    21
@inproceedings{Mueller-Nipkow,
clasohm@1354
    22
author={Olaf M\"uller and Tobias Nipkow},
clasohm@1354
    23
title={Combining Model Checking and Deduction for {I/O}-Automata},
clasohm@1354
    24
booktitle={Proc.\ TACAS Workshop},
clasohm@1354
    25
organization={Aarhus University, BRICS report},
clasohm@1354
    26
year=1995}
clasohm@1354
    27
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
clasohm@1354
    28
clasohm@1354
    29
Should be executed in the subdirectory HOL/IOA/ABP.
clasohm@1354
    30
*)
clasohm@1354
    31
clasohm@1354
    32
goals_limit := 1;
clasohm@1354
    33
clasohm@1354
    34
(*Load theories from ../meta_theory without generating HTML files
clasohm@1354
    35
  (has already been done by NTP/ROOT.ML)*)
clasohm@1354
    36
val old_make_html = !make_html;
clasohm@1354
    37
make_html := false;
clasohm@1354
    38
loadpath := ["../meta_theory"];
clasohm@1354
    39
clasohm@1354
    40
use_thy "Solve";
clasohm@1354
    41
clasohm@1354
    42
make_html := old_make_html;
clasohm@1354
    43
loadpath := ["."];
clasohm@1354
    44
clasohm@1354
    45
clasohm@1354
    46
use_thy "Correctness";