# HG changeset patch
# User haftmann
# Date 1242734251 -7200
# Node ID 52d332f8f909db18757cb85ac22c7766c453bd42
# Parent  82ff416d7d6628fcdbb806f43994ce6dce6af437
pretty printing of functional combinators for evaluation code

diff -r 82ff416d7d66 -r 52d332f8f909 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Fun.thy	Tue May 19 13:57:31 2009 +0200
@@ -100,6 +100,9 @@
 lemma fcomp_id [simp]: "f o> id = f"
   by (simp add: fcomp_def)
 
+code_const fcomp
+  (Eval infixl 1 "#>")
+
 no_notation fcomp (infixl "o>" 60)
 
 
diff -r 82ff416d7d66 -r 52d332f8f909 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon May 18 15:45:42 2009 +0200
+++ b/src/HOL/Product_Type.thy	Tue May 19 13:57:31 2009 +0200
@@ -726,6 +726,9 @@
 lemma fcomp_scomp: "(f o> g) o\<rightarrow> h = f o> (g o\<rightarrow> h)"
   by (simp add: expand_fun_eq scomp_apply fcomp_apply)
 
+code_const scomp
+  (Eval infixl 3 "#->")
+
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)