# HG changeset patch
# User wenzelm
# Date 863440280 -7200
# Node ID 73473cb66bcf6a113cfdda8d2ae0ab418d037fbc
# Parent  85c43ea848ddc72cf1912dbfb9111937fa9ab1fd
partially adapted to axclass / instance;

diff -r 85c43ea848dd -r 73473cb66bcf src/HOLCF/ex/Classlib.thy
--- a/src/HOLCF/ex/Classlib.thy	Mon May 12 14:24:57 1997 +0200
+++ b/src/HOLCF/ex/Classlib.thy	Mon May 12 14:31:20 1997 +0200
@@ -1,17 +1,15 @@
-(*  Title:      FOCUS/Classlib.thy
-    ID:         $ $
+(*  Title:      HOLCF/ex/Classlib.thy
+    ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1995 Technical University Munich
 
-Introduce various type classes
+Introduce various type classes.
 
 !!! Has to be adapted to axclasses !!!
 --------------------------------------
 
-the trivial instance for ++ -- ** // is circ
-the trivial instance for .= and .<=  is bullet
 
-the class hierarchy is as follows
+The class hierarchy is as follows:
 
         pcpo 
          |        
@@ -38,55 +36,50 @@
 (* -------------------------------------------------------------------- *)
 (* class cplus with characteristic constant  ++                         *)
  
-classes cplus < pcpo	
+axclass cplus < pcpo	
 
-arities lift :: (term)cplus
+instance lift :: (term)cplus
 
 ops curried 
 	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
 
 
-(* class cplus has no characteristic axioms                             *)
-(* -------------------------------------------------------------------- *)
 
 (* -------------------------------------------------------------------- *)
 (* class cminus with characteristic constant --                         *)
  
-classes cminus < pcpo	
+axclass cminus < pcpo
 
-arities lift :: (term)cminus
+instance lift :: (term)cminus
 
 ops curried 
 	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
 
-(* class cminus has no characteristic axioms                            *)
-(* -------------------------------------------------------------------- *)
+
 
 (* -------------------------------------------------------------------- *)
 (* class ctimes with characteristic constant **                         *)
  
-classes ctimes < pcpo	
+axclass ctimes < pcpo
 
-arities lift :: (term)ctimes
+instance lift :: (term)ctimes
 
 ops curried 
 	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
 
-(* class ctimes has no characteristic axioms                            *)
-(* -------------------------------------------------------------------- *)
+
 
 (* -------------------------------------------------------------------- *)
 (* class cdiv with characteristic constant //                           *)
  
-classes cdiv < pcpo	
+axclass cdiv < pcpo
 
-arities lift :: (term)cdiv
+instance lift :: (term)cdiv
 
 ops curried 
 	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
 
-(* class cdiv has no characteristic axioms                              *)
-(* -------------------------------------------------------------------- *)
+
 
 (* -------------------------------------------------------------------- *)
 (* class per with characteristic constant .=                            *)