equal
deleted
inserted
replaced
811 |
811 |
812 end |
812 end |
813 |
813 |
814 code_printing |
814 code_printing |
815 constant scomp \<rightharpoonup> (Eval) infixl 3 "#->" |
815 constant scomp \<rightharpoonup> (Eval) infixl 3 "#->" |
816 |
|
817 no_notation fcomp (infixl "\<circ>>" 60) |
|
818 no_notation scomp (infixl "\<circ>\<rightarrow>" 60) |
|
819 |
816 |
820 text \<open> |
817 text \<open> |
821 \<^term>\<open>map_prod\<close> --- action of the product functor upon functions. |
818 \<^term>\<open>map_prod\<close> --- action of the product functor upon functions. |
822 \<close> |
819 \<close> |
823 |
820 |