# HG changeset patch
# User clasohm
# Date 816954396 -3600
# Node ID 39506f7281155335625bfa8e1caa1316d99b45ed
# Parent  9873e1d9541fdbf7d798b67ad1976e630a2b1deb
moved from ../ROOT_ABP.ML;
removed make_chart;
theories are now read from the current directory (because of use_dir)

diff -r 9873e1d9541f -r 39506f728115 src/HOL/IOA/ABP/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/ABP/ROOT.ML	Tue Nov 21 12:46:36 1995 +0100
@@ -0,0 +1,46 @@
+(*  Title:      HOL/IOA/ABP/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 (ABP 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/ABP.
+*)
+
+goals_limit := 1;
+
+(*Load theories from ../meta_theory without generating HTML files
+  (has already been done by NTP/ROOT.ML)*)
+val old_make_html = !make_html;
+make_html := false;
+loadpath := ["../meta_theory"];
+
+use_thy "Solve";
+
+make_html := old_make_html;
+loadpath := ["."];
+
+
+use_thy "Correctness";