removed Witness;
authorwenzelm
Mon May 12 14:24:31 1997 +0200 (1997-05-12)
changeset 31546e20bf579edb
parent 3153 5c9be0158a04
child 3155 85c43ea848dd
removed Witness;
src/HOLCF/ex/Classlib.thy
src/HOLCF/ex/ROOT.ML
     1.1 --- a/src/HOLCF/ex/Classlib.thy	Mon May 12 12:10:49 1997 +0200
     1.2 +++ b/src/HOLCF/ex/Classlib.thy	Mon May 12 14:24:31 1997 +0200
     1.3 @@ -5,11 +5,8 @@
     1.4  
     1.5  Introduce various type classes
     1.6  
     1.7 -The type void of HOLCF/One.thy is a witness for all the introduced classes.
     1.8 -Inspect theory Witness.thy for all the proofs. 
     1.9 -
    1.10 -!!! Witness and Claslib have to be adapted to axclasses !!!
    1.11 -------------------------------------------------------------
    1.12 +!!! Has to be adapted to axclasses !!!
    1.13 +--------------------------------------
    1.14  
    1.15  the trivial instance for ++ -- ** // is circ
    1.16  the trivial instance for .= and .<=  is bullet
     2.1 --- a/src/HOLCF/ex/ROOT.ML	Mon May 12 12:10:49 1997 +0200
     2.2 +++ b/src/HOLCF/ex/ROOT.ML	Mon May 12 14:24:31 1997 +0200
     2.3 @@ -12,7 +12,6 @@
     2.4  proof_timing := true;
     2.5  
     2.6  time_use_thy "Classlib";
     2.7 -time_use_thy "Witness";
     2.8  time_use_thy "Dnat";
     2.9  time_use_thy "Dlist";
    2.10  time_use_thy "Stream";