--- a/IMP/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/IMP/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -19,3 +19,6 @@
loadpath := [".","IMP"];
time_use_thy "Properties";
time_use_thy "Equiv";
+
+make_chart (); (*make HTML chart*)
+
--- a/IOA/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/IOA/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -20,3 +20,5 @@
loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
use_thy "Correctness";
+
+make_chart (); (*make HTML chart*)
--- a/Integ/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/Integ/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Integ/ROOT
+(* Title: Old_HOL/Integ/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge
@@ -10,3 +10,5 @@
loadpath := ["Integ"];
time_use_thy "Integ";
+
+make_chart (); (*make HTML chart*)
--- a/Makefile Thu Jun 29 12:29:58 1995 +0200
+++ b/Makefile Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-# $Id$
+# $Id$
#########################################################################
# #
# Makefile for Isabelle (Old_HOL) #
@@ -6,9 +6,9 @@
#########################################################################
#To make the system, cd to this directory and type
-# make -f Makefile
+# make
#To make the system and test it on standard examples, type
-# make -f Makefile test
+# make test
#Environment variable ISABELLECOMP specifies the compiler.
#Environment variable ISABELLEBIN specifies the destination directory.
@@ -38,9 +38,17 @@
case "$(COMP)" in \
poly*) echo 'make_database"$(BIN)/Old_HOL"; quit();' \
| $(COMP) $(BIN)/Pure;\
- echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/Old_HOL;;\
- sml*) echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | \
- $(BIN)/Pure ;;\
+ if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+ | $(COMP) $(BIN)/Old_HOL;\
+ else echo 'open PolyML; exit_use"ROOT";' \
+ | $(COMP) $(BIN)/Old_HOL;\
+ fi;;\
+ sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+ then echo 'init_html (); exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' | $(BIN)/Pure;\
+ else echo 'exit_use"ROOT.ML"; xML"$(BIN)/Old_HOL" banner;' \
+ | $(BIN)/Pure;\
+ fi;;\
*) echo Bad value for ISABELLECOMP: \
$(COMP) is not poly or sml; exit 1;;\
esac
--- a/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -1,10 +1,10 @@
-(* Title: HOL/ROOT.ML
+(* Title: Old_HOL/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
Adds Classical Higher-order Logic to a database containing Pure Isabelle.
-Should be executed in the subdirectory HOL.
+Should be executed in the subdirectory Old_HOL.
*)
val banner = "Higher-Order Logic";
@@ -18,7 +18,6 @@
use "thy_syntax.ML";
use_thy "HOL";
-use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
@@ -86,4 +85,6 @@
init_pps ();
print_depth 8;
+make_chart (); (*make HTML chart*)
+
val HOL_build_completed = (); (*indicate successful build*)
--- a/Subst/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/Subst/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Subst
+(* Title: Old_HOL/Subst/ROOT.ML
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -35,3 +35,5 @@
use_thy "Subst/Subst";
use_thy "Subst/Unifier";
writeln"END: Root file for Substitutions and Unification";
+
+make_chart (); (*make HTML chart*)
--- a/ex/ROOT.ML Thu Jun 29 12:29:58 1995 +0200
+++ b/ex/ROOT.ML Tue Oct 24 14:59:17 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/ROOT
+(* Title: Old_HOL/ex/ROOT.ML
ID: $Id$
Author: Tobias Nipkow, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
@@ -28,4 +28,7 @@
time_use_thy "Term";
time_use_thy "Simult";
time_use_thy "MT";
+
+make_chart (); (*make HTML chart*)
+
writeln "END: Root file for HOL examples";