--- a/src/HOLCF/Cfun1.thy Thu Jun 29 16:16:24 1995 +0200
+++ b/src/HOLCF/Cfun1.thy Thu Jun 29 16:28:40 1995 +0200
@@ -18,8 +18,7 @@
consts
Cfun :: "('a => 'b)set"
- fapp :: "('a -> 'b)=>('a => 'b)" ("(_[_])" [1000,0] 1000)
- (* usually Rep_Cfun *)
+ fapp :: "('a -> 'b)=>('a => 'b)" (* usually Rep_Cfun *)
(* application *)
fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10)
@@ -28,18 +27,24 @@
less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
-rules
+syntax "@fapp" :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999)
+
+translations "f`x" == "fapp f x"
- Cfun_def "Cfun == {f. contX(f)}"
+defs
+ 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 )"
end