diff --git a/Admin/Linux/Isabelle_app b/Admin/Linux/Isabelle_app
--- a/Admin/Linux/Isabelle_app
+++ b/Admin/Linux/Isabelle_app
@@ -1,28 +1,27 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # Main Isabelle application script.
 
 # minimal Isabelle environment
 
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
 source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
 
 
 # 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
 
 #paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
 unset XMODIFIERS
 
 exec "$ISABELLE_HOME/contrib/jdk/x86_64-linux/jre/bin/java" \
   "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
   -classpath "{CLASSPATH}" \
   "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
   isabelle.Main "$@"
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,835 +1,835 @@
 /*  Title:      Pure/Admin/build_release.scala
     Author:     Makarius
 
 Build full Isabelle distribution from repository.
 */
 
 package isabelle
 
 
 object Build_Release
 {
   /** release info **/
 
   sealed case class Bundle_Info(
     platform: Platform.Family.Value,
     platform_description: String,
     name: String)
   {
     def path: Path = Path.explode(name)
   }
 
   class Release private[Build_Release](
     progress: Progress,
     val date: Date,
     val dist_name: String,
     val dist_dir: Path,
     val dist_version: String,
     val ident: String)
   {
     val isabelle_dir: Path = dist_dir + Path.explode(dist_name)
     val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
     val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
 
     def other_isabelle(dir: Path): Other_Isabelle =
       Other_Isabelle(dir + Path.explode(dist_name),
         isabelle_identifier = dist_name + "-build",
         progress = progress)
 
     def bundle_info(platform: Platform.Family.Value): Bundle_Info =
       platform match {
         case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
         case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
         case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
       }
   }
 
 
 
   /** generated content **/
 
   /* patch release */
 
   private def change_file(dir: Path, name: String, f: String => String)
   {
     val file = dir + Path.explode(name)
     File.write(file, f(File.read(file)))
   }
 
   private val getsettings_file: String = "lib/scripts/getsettings"
 
   private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r
 
   def patch_release(release: Release, is_official: Boolean)
   {
     val dir = release.isabelle_dir
 
     for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala"))
     {
       change_file(dir, name,
         s =>
           s.replaceAllLiterally("val is_identified = false", "val is_identified = true")
            .replaceAllLiterally("val is_official = false", "val is_official = " + is_official))
     }
 
     change_file(dir, getsettings_file,
       s =>
         s.replaceAllLiterally("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident))
          .replaceAllLiterally("ISABELLE_IDENTIFIER=\"\"",
             "ISABELLE_IDENTIFIER=" + quote(release.dist_name)))
 
     change_file(dir, "lib/html/library_index_header.template",
       s => s.replaceAllLiterally("{ISABELLE}", release.dist_name))
 
     for {
       name <-
         List(
           "src/Pure/System/distribution.ML",
           "src/Pure/System/distribution.scala",
           "lib/Tools/version") }
     {
       change_file(dir, name,
         s => s.replaceAllLiterally("repository version", release.dist_version))
     }
 
     change_file(dir, "README",
       s => s.replaceAllLiterally("some repository version of Isabelle", release.dist_version))
   }
 
 
   /* ANNOUNCE */
 
   def make_announce(release: Release)
   {
     File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
 """
 IMPORTANT NOTE
 ==============
 
 This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
 
 """)
   }
 
 
   /* NEWS */
 
   def make_news(other_isabelle: Other_Isabelle, dist_version: String)
   {
     val target = other_isabelle.isabelle_home + Path.explode("doc")
     val target_fonts = target + Path.explode("fonts")
     Isabelle_System.mkdirs(target_fonts)
     other_isabelle.copy_fonts(target_fonts)
 
     HTML.write_document(target, "NEWS.html",
       List(HTML.title("NEWS (" + dist_version + ")")),
       List(
         HTML.chapter("NEWS"),
         HTML.source(
           Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
   }
 
 
   /* bundled components */
 
   class Bundled(platform: Option[Platform.Family.Value] = None)
   {
     def detect(s: String): Boolean =
       s.startsWith("#bundled") && !s.startsWith("#bundled ")
 
     def apply(name: String): String =
       "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
 
     private val Pattern1 = ("""^#bundled:(.*)$""").r
     private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
 
     def unapply(s: String): Option[String] =
       s match {
         case Pattern1(name) => Some(name)
         case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
         case _ => None
       }
   }
 
   def record_bundled_components(dir: Path)
   {
     val catalogs =
       List("main", "bundled").map((_, new Bundled())) :::
       default_platform_families.flatMap(platform =>
         List(platform.toString, "bundled-" + platform.toString).
           map((_, new Bundled(platform = Some(platform)))))
 
     File.append(Components.components(dir),
       terminate_lines("#bundled components" ::
         (for {
           (catalog, bundled) <- catalogs.iterator
           val path = Components.admin(dir) + Path.basic(catalog)
           if path.is_file
           line <- split_lines(File.read(path))
           if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
         } yield bundled(line)).toList))
   }
 
   def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
   {
     val Bundled = new Bundled(platform = Some(platform))
     val components =
       for {
         Bundled(name) <- Components.read_components(dir)
         if !name.startsWith("jedit_build")
       } yield name
     val jdk_component =
       components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
     (components, jdk_component)
   }
 
   def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String])
   {
     def contrib_name(name: String): String =
       Components.contrib(name = name).implode
 
     val Bundled = new Bundled(platform = Some(platform))
     Components.write_components(dir,
       Components.read_components(dir).flatMap(line =>
         line match {
           case Bundled(name) =>
             if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
             else None
           case _ => if (Bundled.detect(line)) None else Some(line)
         }) ::: more_names.map(contrib_name(_)))
   }
 
   def make_contrib(dir: Path)
   {
     Isabelle_System.mkdirs(Components.contrib(dir))
     File.write(Components.contrib(dir, "README"),
 """This directory contains add-on components that contribute to the main
 Isabelle distribution.  Separate licensing conditions apply, see each
 directory individually.
 """)
   }
 
 
 
   /** build release **/
 
   private def execute(dir: Path, script: String): Unit =
     Isabelle_System.bash(script, cwd = dir.file).check
 
   private def execute_tar(dir: Path, args: String): Unit =
     Isabelle_System.gnutar(args, dir = dir).check
 
 
   /* build heaps on remote server */
 
   private def remote_build_heaps(
     options: Options,
     platform: Platform.Family.Value,
     build_sessions: List[String],
     local_dir: Path)
   {
     val server_option = "build_release_server_" + platform.toString
     options.string(server_option) match {
       case SSH.Target(user, host) =>
         using(SSH.open_session(options, host = host, user = user))(ssh =>
         {
           Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
           {
             execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
             ssh.with_tmp_dir(remote_dir =>
             {
               val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
               ssh.write_file(remote_tmp_tar, local_tmp_tar)
               val remote_commands =
                 List(
                   "cd " + File.bash_path(remote_dir),
                   "tar -xf tmp.tar",
                   "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
                   "tar -cf tmp.tar heaps")
               ssh.execute(remote_commands.mkString(" && ")).check
               ssh.read_file(remote_tmp_tar, local_tmp_tar)
             })
             execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
           })
         })
       case s => error("Bad " + server_option + ": " + quote(s))
     }
   }
 
 
   /* main */
 
   private val default_platform_families: List[Platform.Family.Value] =
     List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
 
   def build_release(base_dir: Path,
     options: Options,
     components_base: Path = Components.default_components_base,
     progress: Progress = No_Progress,
     rev: String = "",
     afp_rev: String = "",
     official_release: Boolean = false,
     proper_release_name: Option[String] = None,
     platform_families: List[Platform.Family.Value] = default_platform_families,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_sessions: List[String] = Nil,
     build_library: Boolean = false,
     parallel_jobs: Int = 1): Release =
   {
     val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME"))
 
     val release =
     {
       val date = Date.now()
       val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
       val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute
 
       val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
       val ident =
         try { hg.id(version) }
         catch { case ERROR(_) => error("Bad repository version: " + version) }
 
       val dist_version =
         proper_release_name match {
           case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
           case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
         }
 
       new Release(progress, date, dist_name, dist_dir, dist_version, ident)
     }
 
 
     /* make distribution */
 
     if (release.isabelle_archive.is_file) {
       progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
 
       val archive_ident =
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val getsettings = Path.explode(release.dist_name + "/" + getsettings_file)
             execute_tar(tmp_dir, "-xzf " +
               File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings))
             split_lines(File.read(tmp_dir + getsettings))
               .collectFirst({ case ISABELLE_ID(ident) => ident })
               .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive))
           })
 
       if (release.ident != archive_ident) {
         error("Mismatch of release identification " + release.ident +
           " vs. archive " + archive_ident)
       }
     }
     else {
       progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
 
       Isabelle_System.mkdirs(release.dist_dir)
 
       if (release.isabelle_dir.is_dir)
         error("Directory " + release.isabelle_dir + " already exists")
 
 
       progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
 
       hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
 
       for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
         (release.isabelle_dir + Path.explode(name)).file.delete
       }
 
 
       progress.echo_warning("Preparing distribution " + quote(release.dist_name))
 
       patch_release(release, proper_release_name.isDefined && official_release)
 
       if (proper_release_name.isEmpty) make_announce(release)
 
       make_contrib(release.isabelle_dir)
 
       execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
 
       record_bundled_components(release.isabelle_dir)
 
 
       /* build tools and documentation */
 
       val other_isabelle = release.other_isabelle(release.dist_dir)
 
       other_isabelle.init_settings(
         other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
       other_isabelle.resolve_components(echo = true)
 
       try {
         val export_classpath =
           "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
         other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
         other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
       }
       catch { case ERROR(_) => error("Failed to build tools") }
 
       try {
         other_isabelle.bash(
           "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
       }
       catch { case ERROR(_) => error("Failed to build documentation") }
 
       make_news(other_isabelle, release.dist_version)
 
       for (name <- List("Admin", "browser_info", "heaps")) {
         Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
       }
 
       other_isabelle.cleanup()
 
 
       progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
 
       def execute_dist_name(script: String): Unit =
         Isabelle_System.bash(script, cwd = release.dist_dir.file,
           env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
 
       execute_dist_name("""
 set -e
 
 chmod -R a+r "$DIST_NAME"
 chmod -R u+w "$DIST_NAME"
 chmod -R g=o "$DIST_NAME"
 find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
 """)
 
       execute_tar(release.dist_dir, "-czf " +
         File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
 
       execute_dist_name("""
 set -e
 
 mv "$DIST_NAME" "${DIST_NAME}-old"
 mkdir "$DIST_NAME"
 
 mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
   "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
 mkdir "$DIST_NAME/doc"
 mv "${DIST_NAME}-old/doc/"*.pdf \
   "${DIST_NAME}-old/doc/"*.html \
   "${DIST_NAME}-old/doc/"*.css \
   "${DIST_NAME}-old/doc/fonts" \
   "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
 
 rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
 
 rm -rf "${DIST_NAME}-old"
 """)
     }
 
 
     /* make application bundles */
 
     val bundle_infos = platform_families.map(release.bundle_info)
 
     for (bundle_info <- bundle_infos) {
       val bundle_archive = release.dist_dir + bundle_info.path
       val isabelle_name = release.dist_name
       val platform = bundle_info.platform
 
       progress.echo("\nApplication bundle for " + platform)
 
       Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
       {
         // release archive
 
         execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
         val other_isabelle = release.other_isabelle(tmp_dir)
         val isabelle_target = other_isabelle.isabelle_home
 
 
         // bundled components
 
         progress.echo("Bundled components:")
 
         val contrib_dir = Components.contrib(isabelle_target)
 
         val (bundled_components, jdk_component) =
           get_bundled_components(isabelle_target, platform)
 
         Components.resolve(components_base, bundled_components,
           target_dir = Some(contrib_dir),
           copy_dir = Some(release.dist_dir + Path.explode("contrib")),
           progress = progress)
 
         val more_components_names =
           more_components.map(Components.unpack(contrib_dir, _, progress = progress))
 
         Components.purge(contrib_dir, platform)
 
         activate_components(isabelle_target, platform, more_components_names)
 
 
         // Java parameters
 
         val java_options_title = "# Java runtime options"
         val java_options: List[String] =
           (for {
             variable <-
               List(
                 "ISABELLE_JAVA_SYSTEM_OPTIONS",
                 "JEDIT_JAVA_SYSTEM_OPTIONS",
                 "JEDIT_JAVA_OPTIONS")
             opt <- Word.explode(other_isabelle.getenv(variable))
           } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
 
         val classpath: List[Path] =
         {
           val base = isabelle_target.absolute
           Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
           {
             val abs_path = path.absolute
             File.relative_path(base, abs_path) match {
               case Some(rel_path) => rel_path
               case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
             }
           }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
         }
 
         val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
 
 
         // build heaps
 
         if (build_sessions.nonEmpty) {
           progress.echo("Building heaps ...")
           remote_build_heaps(options, platform, build_sessions, isabelle_target)
         }
 
 
         // application bundling
 
         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")
             File.write(isabelle_app,
               File.read(Path.explode("~~/Admin/Linux/Isabelle_app"))
                 .replaceAllLiterally("{CLASSPATH}",
                   classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
                 .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
             File.set_executable(isabelle_app, true)
 
             val linux_app = isabelle_target + Path.explode("contrib/linux_app")
             File.move(linux_app + Path.explode("Isabelle"),
               isabelle_target + Path.explode(isabelle_name))
             Isabelle_System.rm_tree(linux_app)
 
             val archive_name = isabelle_name + "_linux.tar.gz"
             progress.echo("Packaging " + archive_name + " ...")
             execute_tar(tmp_dir,
               "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
               Bash.string(isabelle_name))
 
 
           case Platform.Family.macos =>
             File.write(isabelle_target + jedit_props,
               File.read(isabelle_target + jedit_props)
                 .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
                 .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
                 .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
                 .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
 
 
             // MacOS application bundle
 
             File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
 
             val isabelle_app = Path.explode(isabelle_name + ".app")
             val app_dir = tmp_dir + isabelle_app
             File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
 
             val app_contents = app_dir + Path.explode("Contents")
             val app_resources = app_contents + Path.explode("Resources")
             File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
 
             File.write(app_contents + Path.explode("Info.plist"),
               File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
                 .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
                 .replaceAllLiterally("{JAVA_OPTIONS}",
                   terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
 
             for (cp <- classpath) {
               File.link(
                 Path.explode("../Resources/" + isabelle_name + "/") + cp,
                 app_contents + Path.explode("Java"),
                 force = true)
             }
 
             File.link(
               Path.explode("../Resources/" + isabelle_name + "/contrib/" +
                 jdk_component + "/x86_64-darwin"),
               app_contents + Path.explode("PlugIns/bundled.jdk"),
               force = true)
 
             File.link(
               Path.explode("../../Info.plist"),
               app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
               force = true)
 
             File.link(
               Path.explode("Contents/Resources/" + isabelle_name),
               app_dir + Path.explode("Isabelle"),
               force = true)
 
 
             // application archive
 
             val archive_name = isabelle_name + "_macos.tar.gz"
             progress.echo("Packaging " + archive_name + " ...")
             execute_tar(tmp_dir,
               "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
               File.bash_path(isabelle_app))
 
 
           case Platform.Family.windows =>
             File.write(isabelle_target + jedit_props,
               File.read(isabelle_target + jedit_props)
                 .replaceAll("lookAndFeel=.*",
                   "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
                 .replaceAll("foldPainter=.*", "foldPainter=Square"))
 
 
             // application launcher
 
             File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
 
             val app_template = Path.explode("~~/Admin/Windows/launch4j")
 
             File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
               (java_options_title :: java_options).map(_ + "\r\n").mkString)
 
             val isabelle_xml = Path.explode("isabelle.xml")
             val isabelle_exe = Path.explode(isabelle_name + ".exe")
 
             File.write(tmp_dir + isabelle_xml,
               File.read(app_template + isabelle_xml)
                 .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
                 .replaceAllLiterally("{OUTFILE}",
                   File.platform_path(isabelle_target + isabelle_exe))
                 .replaceAllLiterally("{ICON}",
                   File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
                 .replaceAllLiterally("{SPLASH}",
                   File.platform_path(app_template + Path.explode("isabelle.bmp")))
                 .replaceAllLiterally("{CLASSPATH}",
                   cat_lines(classpath.map(cp =>
                     "    <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
                 .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
 
             execute(tmp_dir,
               "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
 
             File.copy(app_template + Path.explode("manifest.xml"),
               isabelle_target + isabelle_exe.ext("manifest"))
 
 
             // Cygwin setup
 
             val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
 
             File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
 
             val cygwin_mirror =
               File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
 
             val cygwin_bat = Path.explode("Cygwin-Setup.bat")
             File.write(isabelle_target + cygwin_bat,
               File.read(cygwin_template + cygwin_bat)
                 .replaceAllLiterally("{MIRROR}", cygwin_mirror))
             File.set_executable(isabelle_target + cygwin_bat, true)
 
             for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
               val path = Path.explode(name)
               File.copy(cygwin_template + path,
                 isabelle_target + Path.explode("contrib/cygwin") + path)
             }
 
             execute(isabelle_target,
               """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
               (if (Platform.is_macos) "-perm +100" else "-executable") +
               " -print0 > contrib/cygwin/isabelle/executables")
 
             execute(isabelle_target,
               """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
               """> contrib/cygwin/isabelle/symlinks""")
 
             execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
 
             File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
 
 
             // executable archive (self-extracting 7z)
 
             val archive_name = isabelle_name + ".7z"
             val exe_archive = tmp_dir + Path.explode(archive_name)
             exe_archive.file.delete
 
             progress.echo("Packaging " + archive_name + " ...")
             execute(tmp_dir,
               "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
             if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
 
             val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
             val sfx_txt =
               File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
                 replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
 
             Bytes.write(release.dist_dir + isabelle_exe,
               Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
             File.set_executable(release.dist_dir + isabelle_exe, true)
         }
       })
       progress.echo("DONE")
     }
 
 
     /* minimal website */
 
     for (dir <- website) {
       val website_platform_bundles =
         for {
           bundle_info <- bundle_infos
           if (release.dist_dir + bundle_info.path).is_file
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
         HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
           HTML.text("Isabelle/" + release.ident))
       val afp_link =
         HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
 
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
         List(
           HTML.section(release.dist_name + " (" + release.ident + ")"),
           HTML.subsection("Platforms"),
           HTML.itemize(
             website_platform_bundles.map({ case (bundle, bundle_info) =>
               List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
           HTML.subsection("Repositories"),
           HTML.itemize(
             List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
 
       for ((bundle, _) <- website_platform_bundles)
         File.copy(release.dist_dir + Path.explode(bundle), dir)
     }
 
 
     /* HTML library */
 
     if (build_library) {
       if (release.isabelle_library_archive.is_file) {
         progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
       }
       else {
         Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
           {
             val bundle =
               release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
             execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
 
             val other_isabelle = release.other_isabelle(tmp_dir)
 
             Isabelle_System.mkdirs(other_isabelle.etc)
             File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
 
             other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
               " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
               " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
             other_isabelle.isabelle_home_user.file.delete
 
             execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
             execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
             execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
               " " + Bash.string(release.dist_name + "/browser_info"))
           })
       }
     }
 
     release
   }
 
 
 
   /** command line entry point **/
 
   def main(args: Array[String])
   {
     Command_Line.tool0 {
       var afp_rev = ""
       var components_base: Path = Components.default_components_base
       var official_release = false
       var proper_release_name: Option[String] = None
       var website: Option[Path] = None
       var build_sessions: List[String] = Nil
       var more_components: List[Path] = Nil
       var parallel_jobs = 1
       var build_library = false
       var options = Options.init()
       var platform_families = default_platform_families
       var rev = ""
 
       val getopts = Getopts("""
 Usage: Admin/build_release [OPTIONS] BASE_DIR
 
   Options are:
     -A REV       corresponding AFP changeset id
     -C DIR       base directory for Isabelle components (default: """ +
         Components.default_components_base + """)
     -O           official release (not release-candidate)
     -R RELEASE   proper release with name
     -W WEBSITE   produce minimal website in given directory
     -b SESSIONS  build platform-specific session images (separated by commas)
     -c ARCHIVE   clean bundling with additional component .tar.gz archive
     -j INT       maximum number of parallel jobs (default 1)
     -l           build library
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NAMES     platform families (default: """ + default_platform_families.mkString(",") + """)
     -r REV       Mercurial changeset id (default: RELEASE or tip)
 
   Build Isabelle release in base directory, using the local repository clone.
 """,
         "A:" -> (arg => afp_rev = arg),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "O" -> (_ => official_release = true),
         "R:" -> (arg => proper_release_name = Some(arg)),
         "W:" -> (arg => website = Some(Path.explode(arg))),
         "b:" -> (arg => build_sessions = space_explode(',', arg)),
         "c:" -> (arg =>
           {
             val path = Path.explode(arg)
             Components.Archive.get_name(path.file_name)
             more_components = more_components ::: List(path)
           }),
         "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
         "l" -> (_ => build_library = true),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
         "r:" -> (arg => rev = arg))
 
       val more_args = getopts(args)
       val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() }
 
       val progress = new Console_Progress()
 
       if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
         error("Building for windows requires 7z")
 
       build_release(Path.explode(base_dir), options, components_base = components_base,
         progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release,
         proper_release_name = proper_release_name, website = website,
         platform_families =
           if (platform_families.isEmpty) default_platform_families
           else platform_families,
         more_components = more_components, build_sessions = build_sessions,
         build_library = build_library, parallel_jobs = parallel_jobs)
     }
   }
 }
diff --git a/src/ZF/ZF_Base.thy b/src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy
+++ b/src/ZF/ZF_Base.thy
@@ -1,650 +1,650 @@
 (*  Title:      ZF/ZF_Base.thy
     Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Base of Zermelo-Fraenkel Set Theory\<close>
 
 theory ZF_Base
 imports FOL
 begin
 
 subsection \<open>Signature\<close>
 
 declare [[eta_contract = false]]
 
 typedecl i
 instance i :: "term" ..
 
 axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<in>\<close> 50)  \<comment> \<open>membership relation\<close>
   and zero :: "i"  (\<open>0\<close>)  \<comment> \<open>the empty set\<close>
   and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
   and Inf :: "i"  \<comment> \<open>infinite set\<close>
   and Union :: "i \<Rightarrow> i"  (\<open>\<Union>_\<close> [90] 90)
   and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
 
 abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<notin>\<close> 50)  \<comment> \<open>negated membership relation\<close>
   where "x \<notin> y \<equiv> \<not> (x \<in> y)"
 
 
 subsection \<open>Bounded Quantifiers\<close>
 
 definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
 
 definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
 
 syntax
   "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<forall>_\<in>_./ _)\<close> 10)
   "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  (\<open>(3\<exists>_\<in>_./ _)\<close> 10)
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
 
 
 subsection \<open>Variations on Replacement\<close>
 
 (* Derived form of replacement, restricting P to its functional part.
    The resulting set (for functional P) is the same as with
    PrimReplace, but the rules are simpler. *)
 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
   where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
 
 syntax
   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  (\<open>(1{_ ./ _ \<in> _, _})\<close>)
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
 
 (* Functional form of replacement -- analgous to ML's map functional *)
 
 definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
 
 syntax
   "_RepFun" :: "[i, pttrn, i] => i"  (\<open>(1{_ ./ _ \<in> _})\<close> [51,0,51])
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
 
 (* Separation and Pairing can be derived from the Replacement
    and Powerset Axioms using the following definitions. *)
 definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
   where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
 
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(1{_ \<in> _ ./ _})\<close>)
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
 
 
 subsection \<open>General union and intersection\<close>
 
 definition Inter :: "i => i"  (\<open>\<Inter>_\<close> [90] 90)
   where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
 
 syntax
   "_UNION" :: "[pttrn, i, i] => i"  (\<open>(3\<Union>_\<in>_./ _)\<close> 10)
   "_INTER" :: "[pttrn, i, i] => i"  (\<open>(3\<Inter>_\<in>_./ _)\<close> 10)
 translations
   "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
   "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
 
 
 subsection \<open>Finite sets and binary operations\<close>
 
 (*Unordered pairs (Upair) express binary union/intersection and cons;
   set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
 
 definition Upair :: "[i, i] => i"
   where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
 
 definition Subset :: "[i, i] \<Rightarrow> o"  (infixl \<open>\<subseteq>\<close> 50)  \<comment> \<open>subset relation\<close>
   where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
 
 definition Diff :: "[i, i] \<Rightarrow> i"  (infixl \<open>-\<close> 65)  \<comment> \<open>set difference\<close>
   where "A - B == { x\<in>A . ~(x\<in>B) }"
 
 definition Un :: "[i, i] \<Rightarrow> i"  (infixl \<open>\<union>\<close> 65)  \<comment> \<open>binary union\<close>
   where "A \<union> B == \<Union>(Upair(A,B))"
 
 definition Int :: "[i, i] \<Rightarrow> i"  (infixl \<open>\<inter>\<close> 70)  \<comment> \<open>binary intersection\<close>
   where "A \<inter> B == \<Inter>(Upair(A,B))"
 
 definition cons :: "[i, i] => i"
   where "cons(a,A) == Upair(a,a) \<union> A"
 
 definition succ :: "i => i"
   where "succ(i) == cons(i, i)"
 
 nonterminal "is"
 syntax
   "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
   "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
   "_Finset" :: "is \<Rightarrow> i"  (\<open>{(_)}\<close>)
 translations
   "{x, xs}" == "CONST cons(x, {xs})"
   "{x}" == "CONST cons(x, 0)"
 
 
 subsection \<open>Axioms\<close>
 
 (* ZF axioms -- see Suppes p.238
    Axioms for Union, Pow and Replace state existence only,
    uniqueness is derivable using extensionality. *)
 
 axiomatization
 where
   extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
   Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
   Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
 
   (*We may name this set, though it is not uniquely defined.*)
   infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
 
   (*This formulation facilitates case analysis on A.*)
   foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
 
   (*Schema axiom since predicate P is a higher-order variable*)
   replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
                          b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
 
 
 subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
 
 definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder \<open>THE \<close> 10)
   where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
 
 definition If :: "[o, i, i] \<Rightarrow> i"  (\<open>(if (_)/ then (_)/ else (_))\<close> [10] 10)
   where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
 
 abbreviation (input)
   old_if :: "[o, i, i] => i"  (\<open>if '(_,_,_')\<close>)
   where "if(P,a,b) == If(P,a,b)"
 
 
 subsection \<open>Ordered Pairing\<close>
 
 (* this "symmetric" definition works better than {{a}, {a,b}} *)
 definition Pair :: "[i, i] => i"
   where "Pair(a,b) == {{a,a}, {a,b}}"
 
 definition fst :: "i \<Rightarrow> i"
   where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
 
 definition snd :: "i \<Rightarrow> i"
   where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
 
 definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
   where "split(c) == \<lambda>p. c(fst(p), snd(p))"
 
 (* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
 nonterminal patterns
 syntax
   "_pattern"  :: "patterns => pttrn"         (\<open>\<langle>_\<rangle>\<close>)
   ""          :: "pttrn => patterns"         (\<open>_\<close>)
   "_patterns" :: "[pttrn, patterns] => patterns"  (\<open>_,/_\<close>)
   "_Tuple"    :: "[i, is] => i"              (\<open>\<langle>(_,/ _)\<rangle>\<close>)
 translations
   "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
   "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
   "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
   "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
 
 definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
 
 abbreviation cart_prod :: "[i, i] => i"  (infixr \<open>\<times>\<close> 80)  \<comment> \<open>Cartesian product\<close>
   where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
 
 
 subsection \<open>Relations and Functions\<close>
 
 (*converse of relation r, inverse of function*)
 definition converse :: "i \<Rightarrow> i"
   where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
 
 definition domain :: "i \<Rightarrow> i"
   where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
 
 definition range :: "i \<Rightarrow> i"
   where "range(r) == domain(converse(r))"
 
 definition field :: "i \<Rightarrow> i"
   where "field(r) == domain(r) \<union> range(r)"
 
 definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
   where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
 
 definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
   where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
 
 definition Image :: "[i, i] \<Rightarrow> i"  (infixl \<open>``\<close> 90)  \<comment> \<open>image\<close>
   where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
 
 definition vimage :: "[i, i] \<Rightarrow> i"  (infixl \<open>-``\<close> 90)  \<comment> \<open>inverse image\<close>
   where vimage_def: "r -`` A == converse(r)``A"
 
 (* Restrict the relation r to the domain A *)
 definition restrict :: "[i, i] \<Rightarrow> i"
   where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
 
 
 (* Abstraction, application and Cartesian product of a family of sets *)
 
 definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
 
 definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl \<open>`\<close> 90)  \<comment> \<open>function application\<close>
   where "f`a == \<Union>(f``{a})"
 
 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 *)
 
 syntax
   "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3\<Prod>_\<in>_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3\<Sum>_\<in>_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3\<lambda>_\<in>_./ _)\<close> 10)
 translations
   "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
   "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
   "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
 
 
 subsection \<open>ASCII syntax\<close>
 
 notation (ASCII)
   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)
 
 syntax (ASCII)
   "_Ball"     :: "[pttrn, i, o] => o"        (\<open>(3ALL _:_./ _)\<close> 10)
   "_Bex"      :: "[pttrn, i, o] => o"        (\<open>(3EX _:_./ _)\<close> 10)
   "_Collect"  :: "[pttrn, i, o] => i"        (\<open>(1{_: _ ./ _})\<close>)
   "_Replace"  :: "[pttrn, pttrn, i, o] => i" (\<open>(1{_ ./ _: _, _})\<close>)
   "_RepFun"   :: "[i, pttrn, i] => i"        (\<open>(1{_ ./ _: _})\<close> [51,0,51])
   "_UNION"    :: "[pttrn, i, i] => i"        (\<open>(3UN _:_./ _)\<close> 10)
   "_INTER"    :: "[pttrn, i, i] => i"        (\<open>(3INT _:_./ _)\<close> 10)
   "_PROD"     :: "[pttrn, i, i] => i"        (\<open>(3PROD _:_./ _)\<close> 10)
   "_SUM"      :: "[pttrn, i, i] => i"        (\<open>(3SUM _:_./ _)\<close> 10)
   "_lam"      :: "[pttrn, i, i] => i"        (\<open>(3lam _:_./ _)\<close> 10)
   "_Tuple"    :: "[i, is] => i"              (\<open><(_,/ _)>\<close>)
   "_pattern"  :: "patterns => pttrn"         (\<open><_>\<close>)
 
 
 subsection \<open>Substitution\<close>
 
 (*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
 lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
 by (erule ssubst, assumption)
 
 
 subsection\<open>Bounded universal quantifier\<close>
 
 lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
 by (simp add: Ball_def)
 
 lemmas strip = impI allI ballI
 
 lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
 by (simp add: Ball_def)
 
 (*Instantiates x first: better for automatic theorem proving?*)
 lemma rev_ballE [elim]:
     "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"
 by (simp add: Ball_def, blast)
 
 lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"
 by blast
 
 (*Used in the datatype package*)
 lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
 by (simp add: Ball_def)
 
 (*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
 lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
 by (simp add: Ball_def)
 
 (*Congruence rule for rewriting*)
 lemma ball_cong [cong]:
     "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
 by (simp add: Ball_def)
 
 lemma atomize_ball:
     "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
   by (simp only: Ball_def atomize_all atomize_imp)
 
 lemmas [symmetric, rulify] = atomize_ball
   and [symmetric, defn] = atomize_ball
 
 
 subsection\<open>Bounded existential quantifier\<close>
 
 lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
 by (simp add: Bex_def, blast)
 
 (*The best argument order when there is only one @{term"x\<in>A"}*)
 lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
 by blast
 
 (*Not of the general form for such rules. The existential quanitifer becomes universal. *)
 lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
 by blast
 
 lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
 by (simp add: Bex_def, blast)
 
 (*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
 lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
 by (simp add: Bex_def)
 
 lemma bex_cong [cong]:
     "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]
      ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
 by (simp add: Bex_def cong: conj_cong)
 
 
 
 subsection\<open>Rules for subsets\<close>
 
 lemma subsetI [intro!]:
     "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
 by (simp add: subset_def)
 
 (*Rule in Modus Ponens style [was called subsetE] *)
 lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"
 apply (unfold subset_def)
 apply (erule bspec, assumption)
 done
 
 (*Classical elimination rule*)
 lemma subsetCE [elim]:
     "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"
 by (simp add: subset_def, blast)
 
 (*Sometimes useful with premises in this order*)
 lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
 by blast
 
 lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
 by blast
 
 lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"
 by blast
 
 lemma subset_refl [simp]: "A \<subseteq> A"
 by blast
 
 lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
 by blast
 
 (*Useful for proving A<=B by rewriting in some cases*)
 lemma subset_iff:
      "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
 apply (unfold subset_def Ball_def)
 apply (rule iff_refl)
 done
 
 text\<open>For calculations\<close>
 declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
 
 
 subsection\<open>Rules for equality\<close>
 
 (*Anti-symmetry of the subset relation*)
 lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"
 by (rule extension [THEN iffD2], rule conjI)
 
 
 lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
 by (rule equalityI, blast+)
 
 lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
 lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
 
 lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
 by (blast dest: equalityD1 equalityD2)
 
 lemma equalityCE:
     "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"
 by (erule equalityE, blast)
 
 lemma equality_iffD:
   "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
   by auto
 
 
 subsection\<open>Rules for Replace -- the derived form of replacement\<close>
 
 lemma Replace_iff:
     "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
 apply (unfold Replace_def)
 apply (rule replacement [THEN iff_trans], blast+)
 done
 
 (*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
 lemma ReplaceI [intro]:
     "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>
      b \<in> {y. x\<in>A, P(x,y)}"
 by (rule Replace_iff [THEN iffD2], blast)
 
 (*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
 lemma ReplaceE:
     "[| b \<in> {y. x\<in>A, P(x,y)};
         !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
      |] ==> R"
 by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
 
 (*As above but without the (generally useless) 3rd assumption*)
 lemma ReplaceE2 [elim!]:
     "[| b \<in> {y. x\<in>A, P(x,y)};
         !!x. [| x: A;  P(x,b) |] ==> R
      |] ==> R"
 by (erule ReplaceE, blast)
 
 lemma Replace_cong [cong]:
     "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
      Replace(A,P) = Replace(B,Q)"
 apply (rule equality_iffI)
 apply (simp add: Replace_iff)
 done
 
 
 subsection\<open>Rules for RepFun\<close>
 
 lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
 by (simp add: RepFun_def Replace_iff, blast)
 
 (*Useful for coinduction proofs*)
 lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
 apply (erule ssubst)
 apply (erule RepFunI)
 done
 
 lemma RepFunE [elim!]:
     "[| b \<in> {f(x). x\<in>A};
         !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>
      P"
 by (simp add: RepFun_def Replace_iff, blast)
 
 lemma RepFun_cong [cong]:
     "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
 by (simp add: RepFun_def)
 
 lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
 by (unfold Bex_def, blast)
 
 lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
 by blast
 
 
 subsection\<open>Rules for Collect -- forming a subset by separation\<close>
 
 (*Separation is derivable from Replacement*)
 lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
 by (unfold Collect_def, blast)
 
 lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"
 by simp
 
 lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
 by simp
 
 lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
 by (erule CollectE, assumption)
 
 lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
 by (erule CollectE, assumption)
 
 lemma Collect_cong [cong]:
     "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]
      ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
 by (simp add: Collect_def)
 
 
 subsection\<open>Rules for Unions\<close>
 
 declare Union_iff [simp]
 
 (*The order of the premises presupposes that C is rigid; A may be flexible*)
 lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"
 by (simp, blast)
 
 lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
 by (simp, blast)
 
 
 subsection\<open>Rules for Unions of families\<close>
 (* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
 
 lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
 by (simp add: Bex_def, blast)
 
 (*The order of the premises presupposes that A is rigid; b may be flexible*)
 lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
 by (simp, blast)
 
 
 lemma UN_E [elim!]:
     "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
 by blast
 
 lemma UN_cong:
     "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
 by simp
 
 
 (*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
 
 (* UN_E appears before UnionE so that it is tried first, to avoid expensive
   calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
   the search space.*)
 
 
 subsection\<open>Rules for the empty set\<close>
 
 (*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
   See Suppes, page 21.*)
 lemma not_mem_empty [simp]: "a \<notin> 0"
 apply (cut_tac foundation)
 apply (best dest: equalityD2)
 done
 
 lemmas emptyE [elim!] = not_mem_empty [THEN notE]
 
 
 lemma empty_subsetI [simp]: "0 \<subseteq> A"
 by blast
 
 lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
 by blast
 
 lemma equals0D [dest]: "A=0 ==> a \<notin> A"
 by blast
 
 declare sym [THEN equals0D, dest]
 
 lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
 by blast
 
 lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"
 by blast
 
 
 subsection\<open>Rules for Inter\<close>
 
 (*Not obviously useful for proving InterI, InterD, InterE*)
 lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
 by (simp add: Inter_def Ball_def, blast)
 
 (* Intersection is well-behaved only if the family is non-empty! *)
 lemma InterI [intro!]:
     "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
 by (simp add: Inter_iff)
 
 (*A "destruct" rule -- every B in C contains A as an element, but
   A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
 lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"
 by (unfold Inter_def, blast)
 
 (*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
 lemma InterE [elim]:
     "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"
 by (simp add: Inter_def, blast)
 
 
 subsection\<open>Rules for Intersections of families\<close>
 
 (* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
 
 lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
 by (force simp add: Inter_def)
 
 lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
 by blast
 
 lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
 by blast
 
 lemma INT_cong:
     "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
 by simp
 
 (*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
 
 
 subsection\<open>Rules for Powersets\<close>
 
 lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
 by (erule Pow_iff [THEN iffD2])
 
 lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
 by (erule Pow_iff [THEN iffD1])
 
 declare Pow_iff [iff]
 
 lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment> \<open>\<^term>\<open>0 \<in> Pow(B)\<close>\<close>
 lemmas Pow_top = subset_refl [THEN PowI]         \<comment> \<open>\<^term>\<open>A \<in> Pow(A)\<close>\<close>
 
 
 subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
 
 (*The search is undirected.  Allowing redundant introduction rules may
   make it diverge.  Variable b represents ANY map, such as
   (lam x\<in>A.b(x)): A->Pow(A). *)
 lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
 by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
 
 end