--- a/src/HOLCF/Cfun1.thy Tue Feb 06 12:27:17 1996 +0100
+++ b/src/HOLCF/Cfun1.thy Tue Feb 06 12:42:31 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: HOLCF/cfun1.thy
+(* Title: HOLCF/cfun1.thy
ID: $Id$
- Author: Franz Regensburger
+ Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Definition of the type -> of continuous functions
@@ -14,38 +14,38 @@
types "->" 2 (infixr 5)
-arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
+arities "->" :: (pcpo,pcpo)term (* No properties for ->'s range *)
consts
- Cfun :: "('a => 'b)set"
- fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
- (* application *)
+ Cfun :: "('a => 'b)set"
+ fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
+ (* application *)
- fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
- (* usually Abs_Cfun *)
- (* abstraction *)
+ fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
+ (* usually Abs_Cfun *)
+ (* abstraction *)
- less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
+ less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
translations "f`x" == "fapp f x"
defs
- Cfun_def "Cfun == {f. cont(f)}"
+ Cfun_def "Cfun == {f. cont(f)}"
rules
(*faking a type definition... *)
(* -> is isomorphic to Cfun *)
- Rep_Cfun "fapp fo : Cfun"
- Rep_Cfun_inverse "fabs (fapp fo) = fo"
- Abs_Cfun_inverse "f:Cfun ==> fapp(fabs f) = f"
+ Rep_Cfun "fapp fo : Cfun"
+ Rep_Cfun_inverse "fabs (fapp fo) = fo"
+ Abs_Cfun_inverse "f:Cfun ==> fapp(fabs f) = f"
defs
(*defining the abstract constants*)
- less_cfun_def "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
+ less_cfun_def "less_cfun fo1 fo2 == ( fapp fo1 << fapp fo2 )"
(* start 8bit 1 *)
(* end 8bit 1 *)