--- 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";
--- /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";
--- /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";
--- 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