src/HOL/IOA/ROOT_NTP.ML
author clasohm
Mon Sep 11 12:38:20 1995 +0200 (1995-09-11)
changeset 1253 131f72e2cd56
child 1298 488593372568
permissions -rw-r--r--
split IOA/ROOT.ML into two files for ABP and NTP
clasohm@1253
     1
(*  Title:      HOL/IOA/ROOT_NTP.ML
clasohm@1253
     2
    ID:         $Id$
clasohm@1253
     3
    Author:     Tobias Nipkow & Konrad Slind
clasohm@1253
     4
    Copyright   1994  TU Muenchen
clasohm@1253
     5
clasohm@1253
     6
This is the ROOT file for the theory of I/O-Automata (NTP subdirectory).
clasohm@1253
     7
The formalization is by a semantic model of I/O-Automata.
clasohm@1253
     8
For details see
clasohm@1253
     9
clasohm@1253
    10
@inproceedings{Nipkow-Slind-IOA,
clasohm@1253
    11
author={Tobias Nipkow and Konrad Slind},
clasohm@1253
    12
title={{I/O} Automata in {Isabelle/HOL}},
clasohm@1253
    13
booktitle={Proc.\ TYPES Workshop 1994},
clasohm@1253
    14
publisher=Springer,
clasohm@1253
    15
series=LNCS,
clasohm@1253
    16
note={To appear}}
clasohm@1253
    17
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
clasohm@1253
    18
clasohm@1253
    19
and
clasohm@1253
    20
clasohm@1253
    21
@inproceedings{Mueller-Nipkow,
clasohm@1253
    22
author={Olaf M\"uller and Tobias Nipkow},
clasohm@1253
    23
title={Combining Model Checking and Deduction for {I/O}-Automata},
clasohm@1253
    24
booktitle={Proc.\ TACAS Workshop},
clasohm@1253
    25
organization={Aarhus University, BRICS report},
clasohm@1253
    26
year=1995}
clasohm@1253
    27
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz
clasohm@1253
    28
clasohm@1253
    29
Should be executed in the subdirectory HOL.
clasohm@1253
    30
*)
clasohm@1253
    31
goals_limit := 1;
clasohm@1253
    32
clasohm@1253
    33
loadpath := ["IOA/meta_theory","IOA/NTP"];
clasohm@1253
    34
use_thy "Correctness";