# HG changeset patch
# User wenzelm
# Date 877102347 -7200
# Node ID 176d617a8ba8bc3233f31e438044ac72e64f3d07
# Parent  c036caebfc7540899f33f0e958c6a4cd024b5095
*** empty log message ***

diff -r c036caebfc75 -r 176d617a8ba8 src/HOLCF/ex/Classlib.ML
--- a/src/HOLCF/ex/Classlib.ML	Fri Oct 17 15:25:12 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-open Classlib;
-
diff -r c036caebfc75 -r 176d617a8ba8 src/HOLCF/ex/Classlib.thy
--- a/src/HOLCF/ex/Classlib.thy	Fri Oct 17 15:25:12 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,132 +0,0 @@
-(*  Title:      HOLCF/ex/Classlib.thy
-    ID:         $Id$
-    Author:     Franz Regensburger
-    Copyright   1995 Technical University Munich
-
-Introduce various type classes.
-
-!!! Has to be adapted to axclasses !!!
---------------------------------------
-
-
-The class hierarchy is as follows:
-
-        pcpo 
-         |        
-          ----------------
-         |               | 
-         |      --------------------- 
-         |      |       |      |    | 
-        per   cplus  cminus ctimes cdvi
-         |
-       equiv
-       /  \
-      /    \
-     |     |
-    qpo    eq
-     | 
-     |    
-  qlinear
-
-
-*)
-
-Classlib = HOLCF +
-
-(* -------------------------------------------------------------------- *)
-(* class cplus with characteristic constant  ++                         *)
- 
-axclass cplus < pcpo	
-
-instance lift :: (term)cplus
-
-ops curried 
-	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
-
-
-
-(* -------------------------------------------------------------------- *)
-(* class cminus with characteristic constant --                         *)
- 
-axclass cminus < pcpo
-
-instance lift :: (term)cminus
-
-ops curried 
-	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
-
-
-
-(* -------------------------------------------------------------------- *)
-(* class ctimes with characteristic constant **                         *)
- 
-axclass ctimes < pcpo
-
-instance lift :: (term)ctimes
-
-ops curried 
-	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
-
-
-
-(* -------------------------------------------------------------------- *)
-(* class cdiv with characteristic constant //                           *)
- 
-axclass cdiv < pcpo
-
-instance lift :: (term)cdiv
-
-ops curried 
-	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
-
-
-
-(* -------------------------------------------------------------------- *)
-(* class per with characteristic constant .=                            *)
- 
-classes per < pcpo	
-
-arities lift :: (term)per
-
-ops curried 
-	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
-syntax (symbols)
-	"op .=" :: "'a::per => 'a => tr"	(infixl "\\<doteq>" 55)
-
-rules 
-
-strict_per	"(UU .= x) = UU & (x .= UU) = UU"
-total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
-flat_per	"flat (x::'a::per)"
-
-sym_per		"(x .= y) = (y .= x)"
-trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
-
-(* -------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------- *)
-(* class equiv is a refinement of of class per                          *)
- 
-classes equiv < per 	
-
-arities lift :: (term)equiv
-
-rules 
-
-refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
-
-(* -------------------------------------------------------------------- *)
-
-(* -------------------------------------------------------------------- *)
-(* class eq is a refinement of of class equiv                           *)
- 
-classes eq < equiv  	
-
-arities lift :: (term)eq
-
-rules 
-
-weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
-	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
-
-end
diff -r c036caebfc75 -r 176d617a8ba8 src/HOLCF/ex/Dlist.thy
--- a/src/HOLCF/ex/Dlist.thy	Fri Oct 17 15:25:12 1997 +0200
+++ b/src/HOLCF/ex/Dlist.thy	Fri Oct 17 17:32:27 1997 +0200
@@ -10,18 +10,18 @@
 
 domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
 
-ops curried
+
+consts
 
 lmap	:: "('a -> 'b) -> 'a dlist -> 'b dlist"
-lmem	:: "('a::eq)  -> 'a dlist -> tr"		(cinfixl 50)
+lmem	:: "('a::eq)  -> 'a dlist -> tr"
 
 defs
 
-lmap_def "   lmap Ú fix`(LAM h f s. case s of dnil => dnil 
-				      | x ## xs => f`x ## h`f`xs)"
+lmap_def "lmap == fix`(LAM h f s. case s of dnil => dnil
+			          | x ## xs => f`x ## h`f`xs)"
 
-lmem_def "op lmem Ú fix`(LAM h e l. case l of dnil => FF
-			 | x ## xs => If e Ù x then TT else h`e`xs fi)"
+lmem_def "lmem == fix`(LAM h e l. case l of dnil => FF
+     	 	  		  | x ## xs => If e Ù x then TT else h`e`xs fi)"
 
 end
-