proper print mode for function_space notation (amending d68b705719ce);
authorwenzelm
Wed, 19 Feb 2020 20:00:07 +0100
changeset 71674 8f628d216ea1
parent 71673 4876e6f62fe5
child 71675 ed8d50969995
proper print mode for function_space notation (amending d68b705719ce);
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)