# HG changeset patch
# User traytel
# Date 1582185919 -3600
# Node ID ed8d50969995f4a9c6361f43555a1f881e7222cd
# Parent  5e25a693c5cfff00811b673796a575ca2aae23d1# Parent  8f628d216ea192fdb28896491b411f0f2e381a5a
merged

diff -r 5e25a693c5cf -r ed8d50969995 Admin/Linux/Isabelle_app
--- a/Admin/Linux/Isabelle_app	Wed Feb 19 15:49:10 2020 +0100
+++ b/Admin/Linux/Isabelle_app	Thu Feb 20 09:05:19 2020 +0100
@@ -12,8 +12,7 @@
 
 # Java runtime options
 
-ISABELLE_NAME="$(basename "$0" .run)"
-declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/${ISABELLE_NAME}.options"))
+declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
 
 
 # main
diff -r 5e25a693c5cf -r ed8d50969995 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Feb 19 15:49:10 2020 +0100
+++ b/src/Pure/Admin/build_release.scala	Thu Feb 20 09:05:19 2020 +0100
@@ -506,7 +506,7 @@
 
         platform match {
           case Platform.Family.linux =>
-            File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
+            File.write(isabelle_target + Path.explode("Isabelle.options"),
               terminate_lines(java_options_title :: java_options))
 
             val isabelle_app = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
diff -r 5e25a693c5cf -r ed8d50969995 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Wed Feb 19 15:49:10 2020 +0100
+++ b/src/ZF/ZF_Base.thy	Thu Feb 20 09:05:19 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)