--- 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;
-
--- 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
--- 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
-