# HG changeset patch
# User wenzelm
# Date 1582138807 -3600
# Node ID 8f628d216ea192fdb28896491b411f0f2e381a5a
# Parent  4876e6f62fe57908430a79baf0f3fd4582e40686
proper print mode for function_space notation (amending d68b705719ce);

diff -r 4876e6f62fe5 -r 8f628d216ea1 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Wed Feb 19 15:40:28 2020 +0100
+++ b/src/ZF/ZF_Base.thy	Wed Feb 19 20:00:07 2020 +0100
@@ -242,8 +242,8 @@
 definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
 
-abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr \<open>->\<close> 60)  \<comment> \<open>function space\<close>
-  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr \<open>\<rightarrow>\<close> 60)  \<comment> \<open>function space\<close>
+  where "A \<rightarrow> B \<equiv> Pi(A, \<lambda>_. B)"
 
 
 (* binder syntax *)
@@ -264,7 +264,7 @@
   cart_prod       (infixr \<open>*\<close> 80) and
   Int             (infixl \<open>Int\<close> 70) and
   Un              (infixl \<open>Un\<close> 65) and
-  function_space  (infixr \<open>\<rightarrow>\<close> 60) and
+  function_space  (infixr \<open>->\<close> 60) and
   Subset          (infixl \<open><=\<close> 50) and
   mem             (infixl \<open>:\<close> 50) and
   not_mem         (infixl \<open>~:\<close> 50)