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