src/HOLCF/Cfun1.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 6382 8b0c9205da75
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/cfun1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Definition of the type ->  of continuous functions
     7 
     8 *)
     9 
    10 Cfun1 = Cont +
    11 
    12 default cpo
    13 
    14 typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f. cont f}" (CfunI)
    15 
    16 (* to make << defineable *)
    17 instance "->"  :: (cpo,cpo)sq_ord
    18 
    19 syntax
    20 	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
    21                                                 (* application      *)
    22         Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
    23                                                 (* abstraction      *)
    24         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
    25 
    26 syntax (symbols)
    27   "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
    28   "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
    29 					("(3\\<Lambda>_./ _)" [0, 10] 10)
    30 defs 
    31   less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
    32 
    33 end