# HG changeset patch
# User clasohm
# Date 810815900 -7200
# Node ID 131f72e2cd565e3e8ec63f0a59b5c17df18ec04d
# Parent  27130da22f52dddea2fe9a2d7f6748c8b927e1c3
split IOA/ROOT.ML into two files for ABP and NTP

diff -r 27130da22f52 -r 131f72e2cd56 src/HOL/IOA/ROOT.ML
--- a/src/HOL/IOA/ROOT.ML	Fri Sep 08 14:52:22 1995 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(*  Title:      HOL/IOA/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.
-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.
-*)
-goals_limit := 1;
-
-loadpath := ["IOA/meta_theory","IOA/NTP"];
-use_thy "Correctness";
-
-loadpath := ["IOA/meta_theory","IOA/ABP"];
-use_thy "Correctness";
diff -r 27130da22f52 -r 131f72e2cd56 src/HOL/IOA/ROOT_ABP.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/ROOT_ABP.ML	Mon Sep 11 12:38:20 1995 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/IOA/ROOT_ABP.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.
+*)
+goals_limit := 1;
+
+loadpath := ["IOA/meta_theory","IOA/ABP"];
+use_thy "Correctness";
diff -r 27130da22f52 -r 131f72e2cd56 src/HOL/IOA/ROOT_NTP.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/ROOT_NTP.ML	Mon Sep 11 12:38:20 1995 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/IOA/ROOT_NTP.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.
+*)
+goals_limit := 1;
+
+loadpath := ["IOA/meta_theory","IOA/NTP"];
+use_thy "Correctness";
diff -r 27130da22f52 -r 131f72e2cd56 src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Sep 08 14:52:22 1995 +0200
+++ b/src/HOL/Makefile	Mon Sep 11 12:38:20 1995 +0200
@@ -87,7 +87,8 @@
  $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
 
 IOA:    $(BIN)/HOL  $(IOA_FILES)
-	echo 'exit_use"IOA/ROOT.ML";quit();' | $(LOGIC)
+	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
+	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
 
 ##Properties of substitutions
 SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas