--- a/src/HOLCF/ex/Classlib.thy Mon May 12 12:10:49 1997 +0200
+++ b/src/HOLCF/ex/Classlib.thy Mon May 12 14:24:31 1997 +0200
@@ -5,11 +5,8 @@
Introduce various type classes
-The type void of HOLCF/One.thy is a witness for all the introduced classes.
-Inspect theory Witness.thy for all the proofs.
-
-!!! Witness and Claslib have to be adapted to axclasses !!!
-------------------------------------------------------------
+!!! Has to be adapted to axclasses !!!
+--------------------------------------
the trivial instance for ++ -- ** // is circ
the trivial instance for .= and .<= is bullet
--- a/src/HOLCF/ex/ROOT.ML Mon May 12 12:10:49 1997 +0200
+++ b/src/HOLCF/ex/ROOT.ML Mon May 12 14:24:31 1997 +0200
@@ -12,7 +12,6 @@
proof_timing := true;
time_use_thy "Classlib";
-time_use_thy "Witness";
time_use_thy "Dnat";
time_use_thy "Dlist";
time_use_thy "Stream";