# HG changeset patch
# User wenzelm
# Date 863439871 -7200
# Node ID 6e20bf579edba919bcc720c2eb6c3b9ef04f9b58
# Parent  5c9be0158a04815b4c632d1b56138f0b0a07c969
removed Witness;

diff -r 5c9be0158a04 -r 6e20bf579edb src/HOLCF/ex/Classlib.thy
--- 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
diff -r 5c9be0158a04 -r 6e20bf579edb src/HOLCF/ex/ROOT.ML
--- 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";