# HG changeset patch # User clasohm # Date 816954422 -3600 # Node ID 1c94ebc9089800baf8356fa76576ef9a1a312326 # Parent 39506f7281155335625bfa8e1caa1316d99b45ed moved from ../ROOT_NTP.ML; removed make_chart; theories are now read from the current directory (because of use_dir) diff -r 39506f728115 -r 1c94ebc90898 src/HOL/IOA/NTP/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/IOA/NTP/ROOT.ML Tue Nov 21 12:47:02 1995 +0100 @@ -0,0 +1,35 @@ +(* Title: HOL/IOA/NTP/ROOT.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +This is the ROOT file for the theory of I/O-Automata (NTP subdirectory). +The formalization is by a semantic model of I/O-Automata. +For details see + +@inproceedings{Nipkow-Slind-IOA, +author={Tobias Nipkow and Konrad Slind}, +title={{I/O} Automata in {Isabelle/HOL}}, +booktitle={Proc.\ TYPES Workshop 1994}, +publisher=Springer, +series=LNCS, +note={To appear}} +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz + +and + +@inproceedings{Mueller-Nipkow, +author={Olaf M\"uller and Tobias Nipkow}, +title={Combining Model Checking and Deduction for {I/O}-Automata}, +booktitle={Proc.\ TACAS Workshop}, +organization={Aarhus University, BRICS report}, +year=1995} +ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz + +Should be executed in the subdirectory HOL/IOA/NTP. +*) + +goals_limit := 1; + +loadpath := [".", "../meta_theory"]; +use_thy "Correctness";