src/HOLCF/fun2.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/fun2.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     3
    Author: 	Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Class Instance =>::(term,po)po
nipkow@243
     7
Definiton of least element
nipkow@243
     8
*)
nipkow@243
     9
nipkow@243
    10
Fun2 = Fun1 + 
nipkow@243
    11
nipkow@243
    12
(* default class is still term !*)
nipkow@243
    13
nipkow@243
    14
(* Witness for the above arity axiom is fun1.ML *)
nipkow@243
    15
nipkow@243
    16
arities fun :: (term,po)po
nipkow@243
    17
nipkow@243
    18
consts	
nipkow@243
    19
	UU_fun  :: "'a::term => 'b::pcpo"
nipkow@243
    20
nipkow@243
    21
rules
nipkow@243
    22
nipkow@243
    23
(* instance of << for type ['a::term => 'b::po]  *)
nipkow@243
    24
nipkow@243
    25
inst_fun_po	"(op <<)::['a=>'b::po,'a=>'b::po ]=>bool = less_fun"
nipkow@243
    26
nipkow@243
    27
(* definitions *)
nipkow@243
    28
(* The least element in type 'a::term => 'b::pcpo *)
nipkow@243
    29
nipkow@243
    30
UU_fun_def	"UU_fun == (% x.UU)"
nipkow@243
    31
nipkow@243
    32
end
nipkow@243
    33
nipkow@243
    34
nipkow@243
    35
nipkow@243
    36
nipkow@243
    37
nipkow@243
    38
nipkow@243
    39
nipkow@243
    40