Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added <cdot> syntax for continuous application $.
authornipkow
Wed, 10 Jan 2001 20:41:14 +0100
changeset 10863 fef84fefd33f
parent 10862 857688d775b0
child 10864 f0b0a125ae4b
Added <cdot> syntax for continuous application $.
src/HOLCF/Cfun1.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Cfun1.thy	Wed Jan 10 20:21:11 2001 +0100
+++ b/src/HOLCF/Cfun1.thy	Wed Jan 10 20:41:14 2001 +0100
@@ -17,9 +17,9 @@
 instance "->"  :: (cpo,cpo)sq_ord
 
 syntax
-	Rep_CFun  :: "('a -> 'b)=>('a => 'b)" ("_$_" [999,1000] 999)
+	Rep_CFun  :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
                                                 (* application      *)
-        Abs_CFun  :: "('a => 'b)=>('a -> 'b)"     (binder "LAM " 10)
+        Abs_CFun  :: "('a => 'b) => ('a -> 'b)" (binder "LAM " 10)
                                                 (* abstraction      *)
         less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool"
 
@@ -27,6 +27,11 @@
   "->"		:: [type, type] => type	("(_ \\<rightarrow>/ _)" [1,0]0)
   "LAM "	:: "[idts, 'a => 'b] => ('a -> 'b)"
 					("(3\\<Lambda>_./ _)" [0, 10] 10)
+  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
+
+syntax (HTML output)
+  Rep_CFun      :: "('a -> 'b) => ('a => 'b)"  ("(_\\<cdot>_)" [999,1000] 999)
+
 defs 
   less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
isabelle