--- a/src/CTT/Makefile Thu Mar 20 11:11:53 1997 +0100
+++ b/src/CTT/Makefile Thu Mar 20 11:23:19 1997 +0100
@@ -61,8 +61,8 @@
test: ex/ROOT.ML $(BIN)/CTT $(EX_FILES)
@case `basename "$(COMP)"` in \
- poly*) echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CTT ;;\
- sml*) echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CTT;;\
+ poly*) echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/CTT ;;\
+ sml*) echo 'exit_use_dir"ex";' | $(BIN)/CTT;;\
*) echo Bad value for ISABELLECOMP: \
\"$(COMP)\" is not poly or sml;;\
esac
--- a/src/CTT/ex/ROOT.ML Thu Mar 20 11:11:53 1997 +0100
+++ b/src/CTT/ex/ROOT.ML Thu Mar 20 11:23:19 1997 +0100
@@ -6,15 +6,16 @@
Executes all examples for Constructive Type Theory.
*)
-CTT_build_completed; (*Cause examples to fail if CTT did*)
+writeln"Root file for CTT examples";
-writeln"Root file for CTT examples";
+CTT_build_completed; (*Cause examples to fail if CTT did*)
print_depth 2;
proof_timing := true;
-time_use "ex/typechk.ML";
-time_use "ex/elim.ML";
-time_use "ex/equal.ML";
-time_use "ex/synth.ML";
+time_use "typechk.ML";
+time_use "elim.ML";
+time_use "equal.ML";
+time_use "synth.ML";
+cd "..";
maketest"END: Root file for CTT examples";