src/HOLCF/fun2.thy
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
     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