--- a/NEWS Thu Mar 19 11:57:43 2020 +0100
+++ b/NEWS Sat Mar 21 22:12:21 2020 +0100
@@ -94,6 +94,19 @@
automatic font scaling is usually absent on Linux, in contrast to
Windows and macOS.
+* The default value for the jEdit property "view.antiAlias" (menu item
+Utilities / Global Options / Text Area / Anti Aliased smooth text) is
+now "subpixel HRGB", instead of former "standard". Especially on Linux
+this often leads to faster text rendering, but can also cause problems
+with odd color shades. An alternative is to switch back to "standard"
+here, and set the following Java system property:
+
+ isabelle jedit -Dsun.java2d.opengl=true
+
+This can be made persistent via JEDIT_JAVA_OPTIONS in
+$ISABELLE_HOME_USER/etc/settings. For the "Isabelle2020" desktop
+application there is a corresponding options file in the same directory.
+
*** Isabelle/VSCode Prover IDE ***
@@ -1488,6 +1501,9 @@
is analogous to ISABELLE_PLATFORM, ISABELLE_PLATFORM32,
ISABELLE_PLATFORM64.
+* The command-line tool "isabelle build_docker" has been slightly
+improved: it is now properly documented in the "system" manual.
+
* Command-line tool "isabelle build_docker" builds a Docker image from
the Isabelle application bundle for Linux. See also
https://hub.docker.com/r/makarius/isabelle
--- a/src/Doc/Isar_Ref/Generic.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Sat Mar 21 22:12:21 2020 +0100
@@ -1301,8 +1301,8 @@
The rule \<open>P \<Longrightarrow> P \<or> Q\<close> is unsafe because it reduces \<open>P
\<or> Q\<close> to \<open>P\<close>, which might turn out as premature choice of an
- unprovable subgoal. Any rule is unsafe whose premises contain new
- unknowns. The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
+ unprovable subgoal. Any rule whose premises contain new unknowns is
+ unsafe. The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
unsafe, since it is applied via elim-resolution, which discards the
assumption \<open>\<forall>x. P x\<close> and replaces it by the weaker
assumption \<open>P t\<close>. The rule \<open>P t \<Longrightarrow> \<exists>x. P x\<close> is
@@ -1316,8 +1316,8 @@
that \<open>(\<or>E)\<close> is unsafe, because repeated application of it
could generate exponentially many subgoals. Induction rules are
unsafe because inductive proofs are difficult to set up
- automatically. Any inference is unsafe that instantiates an unknown
- in the proof state --- thus matching must be used, rather than
+ automatically. Any inference that instantiates an unknown
+ in the proof state is unsafe --- thus matching must be used, rather than
unification. Even proof by assumption is unsafe if it instantiates
unknowns shared with other subgoals.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sat Mar 21 22:12:21 2020 +0100
@@ -2434,7 +2434,7 @@
Variant \<open>code nbe\<close> accepts also non-left-linear equations for
\<^emph>\<open>normalization by evaluation\<close> only.
- Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
+ Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
and drop all code equations declared for them. In the case of \<open>abort\<close>,
these constants then do not require to a specification by means of
code equations; if needed these are implemented by program abort (exception)
--- a/src/Doc/Isar_Ref/Proof.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Mar 21 22:12:21 2020 +0100
@@ -1190,10 +1190,10 @@
declared using the @{attribute_def induct_simp} attribute.
The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
- \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
- separate variables by ``\<open>and\<close>'' to generalize them in other goals then the
- first. Thus induction hypotheses may become sufficiently general to get the
- proof through. Together with definitional instantiations, one may
+ \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. It is possible
+ to separate variables by ``\<open>and\<close>'' to generalize in goals other than
+ the first. Thus induction hypotheses may become sufficiently general to get
+ the proof through. Together with definitional instantiations, one may
effectively perform induction over expressions of a certain structure.
The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
--- a/src/Doc/Isar_Ref/Spec.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Mar 21 22:12:21 2020 +0100
@@ -194,7 +194,7 @@
arguments; a syntactic abbreviation links the long form with the abstract
version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local
- abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter
+ abbreviation \<open>a \<equiv> c.a x\<close> in the target context (for the fixed parameter
\<open>x\<close>).
Theorems are exported by discharging the assumptions and generalizing the
@@ -365,7 +365,7 @@
\<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
simultaneously and states axiomatic properties for these. The constants are
marked as being specified once and for all, which prevents additional
- specifications for the same constants later on, but it is always possible do
+ specifications for the same constants later on, but it is always possible to
emit axiomatizations without referring to particular constants. Note that
lack of precise dependency tracking of axiomatizations may disrupt the
well-formedness of an otherwise definitional theory.
@@ -542,7 +542,7 @@
expressions automatically takes care of the most general typing that the
combined context elements may acquire.
- The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
+ The \<open>import\<close> consists of a locale expression; see \secref{sec:locale-expr}
above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are
parameters of the defined locale. Locale parameters whose instantiation is
omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are
@@ -949,7 +949,7 @@
\<^medskip>
Co-regularity is a very fundamental property of the order-sorted algebra of
- types. For example, it entails principle types and most general unifiers,
+ types. For example, it entails principal types and most general unifiers,
e.g.\ see @{cite "nipkow-prehofer"}.
\<close>
--- a/src/Doc/JEdit/JEdit.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sat Mar 21 22:12:21 2020 +0100
@@ -305,7 +305,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2019\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2020\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
@@ -2194,6 +2194,24 @@
\<^bold>\<open>Workaround:\<close> Use action @{action isabelle.draft} and print via the Web
browser.
+ \<^item> \<^bold>\<open>Problem:\<close> Antialiased text rendering may show bad performance or bad
+ visual quality, notably on Linux/X11.
+
+ \<^bold>\<open>Workaround:\<close> The property \<^verbatim>\<open>view.antiAlias\<close> (via menu item Utilities /
+ Global Options / Text Area / Anti Aliased smooth text) has the main impact
+ on text rendering, but some related properties may also change the
+ behaviour. The default is \<^verbatim>\<open>view.antiAlias=subpixel HRGB\<close>: it can be much
+ faster than \<^verbatim>\<open>standard\<close>, but occasionally causes problems with odd color
+ shades. An alternative is to have \<^verbatim>\<open>view.antiAlias=standard\<close> and set a Java
+ system property like this:\<^footnote>\<open>See also
+ \<^url>\<open>https://docs.oracle.com/javase/10/troubleshoot/java-2d-pipeline-rendering-and-properties.htm\<close>.\<close>
+ @{verbatim [display] \<open>isabelle jedit -Dsun.java2d.opengl=true\<close>}
+
+ If this works reliably, it can be made persistent via @{setting
+ JEDIT_JAVA_OPTIONS} within \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. For
+ the Isabelle desktop ``app'', there is a corresponding file with Java
+ runtime options in the main directory (name depends on the OS platform).
+
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
event handling of Java/AWT/Swing.
--- a/src/Doc/System/Environment.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/System/Environment.thy Sat Mar 21 22:12:21 2020 +0100
@@ -58,7 +58,7 @@
\<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2018\<close>.
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2020\<close>.
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
@@ -148,7 +148,7 @@
of the @{executable isabelle} executable.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018\<close>''.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/System/Misc.thy Sat Mar 21 22:12:21 2020 +0100
@@ -11,6 +11,113 @@
alphabetical order.
\<close>
+section \<open>Building Isabelle docker images\<close>
+
+text \<open>
+ Docker\<^footnote>\<open>\<^url>\<open>https://docs.docker.com\<close>\<close> provides a self-contained environment
+ for complex applications called \<^emph>\<open>container\<close>, although it does not fully
+ contain the program in a strict sense of the word. This includes basic
+ operating system services (usually based on Linux), shared libraries and
+ other required packages. Thus Docker is a light-weight alternative to
+ regular virtual machines, or a heavy-weight alternative to conventional
+ self-contained applications.
+
+ Although Isabelle can be easily run on a variety of OS environments without
+ extra containment, Docker images may occasionally be useful when a
+ standardized Linux environment is required, even on
+ Windows\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-windows\<close>\<close> and
+ macOS\<^footnote>\<open>\<^url>\<open>https://docs.docker.com/docker-for-mac\<close>\<close>. Further uses are in
+ common cloud computing environments, where applications need to be submitted
+ as Docker images in the first place.
+
+ \<^medskip>
+ The @{tool_def build_docker} tool builds docker images from a standard
+ Isabelle application archive for Linux:
+
+ @{verbatim [display]
+\<open>Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
+
+ Options are:
+ -B NAME base image (default "ubuntu")
+ -E set bin/isabelle as entrypoint
+ -P NAME additional Ubuntu package collection ("X11", "latex")
+ -l NAME default logic (default ISABELLE_LOGIC="HOL")
+ -n no docker build
+ -o FILE output generated Dockerfile
+ -p NAME additional Ubuntu package
+ -t TAG docker build tag
+ -v verbose
+
+ Build Isabelle docker image with default logic image, using a standard
+ Isabelle application archive for Linux (local file or remote URL).\<close>}
+
+ Option \<^verbatim>\<open>-E\<close> sets \<^verbatim>\<open>bin/isabelle\<close> of the contained Isabelle distribution as
+ the standard entry point of the Docker image. Thus \<^verbatim>\<open>docker run\<close> will
+ imitate the \<^verbatim>\<open>isabelle\<close> command-line tool (\secref{sec:isabelle-tool}) of a
+ regular local installation, but it lacks proper GUI support: \<^verbatim>\<open>isabelle jedit\<close>
+ will not work without further provisions. Note that the default entrypoint
+ may be changed later via \<^verbatim>\<open>docker run --entrypoint="..."\<close>.
+
+ Option \<^verbatim>\<open>-t\<close> specifies the Docker image tag: this a symbolic name within the
+ local Docker name space, but also relevant for Docker
+ Hub\<^footnote>\<open>\<^url>\<open>https://hub.docker.com\<close>\<close>.
+
+ Option \<^verbatim>\<open>-l\<close> specifies the default logic image of the Isabelle distribution
+ contained in the Docker environment: it will be produced by \<^verbatim>\<open>isabelle build -b\<close>
+ as usual (\secref{sec:tool-build}) and stored within the image.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the
+ Isabelle installation: it needs to be a suitable version of Ubuntu Linux.
+ The default \<^verbatim>\<open>ubuntu\<close> refers to the latest LTS version provided by Canonical
+ as the official Ubuntu vendor\<^footnote>\<open>\<^url>\<open>https://hub.docker.com/_/ubuntu\<close>\<close>. For
+ Isabelle2020 this should be Ubuntu 18.04 LTS.
+
+ Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology
+ of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution.
+
+ Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as
+ provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 18.04 LTS). This
+ imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will
+ only provide remote X11 support according to the modest GUI quality
+ standards of the late 1990-ies.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close>
+ outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a
+ Dockerfile only, which might be useful for informative purposes or other
+ tools.
+
+ Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Produce a Dockerfile (without image) from a remote Isabelle distribution:
+ @{verbatim [display]
+\<open> isabelle build_docker -E -n -o Dockerfile
+ https://isabelle.in.tum.de/website-Isabelle2020/dist/Isabelle2020_linux.tar.gz\<close>}
+
+ Build a standard Isabelle Docker image from a local Isabelle distribution,
+ with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
+
+ @{verbatim [display]
+\<open> isabelle build_docker -E -t test/isabelle:Isabelle2020 Isabelle2020_linux.tar.gz\<close>}
+
+ Invoke the raw Isabelle/ML process within that image:
+ @{verbatim [display]
+\<open> docker run test/isabelle:Isabelle2020 process -e "Session.welcome ()"\<close>}
+
+ Invoke a Linux command-line tool within the contained Isabelle system
+ environment:
+ @{verbatim [display]
+\<open> docker run test/isabelle:Isabelle2020 env uname -a\<close>}
+ The latter should always report a Linux operating system, even when running
+ on Windows or macOS.
+\<close>
+
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close>
@@ -267,7 +374,7 @@
\<^medskip>
The default is to output the full version string of the Isabelle
- distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2018: August 2018\<close>.
+ distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2020: April 2020\<close>.
The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
id of the @{setting ISABELLE_HOME} directory.
--- a/src/Doc/manual.bib Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Doc/manual.bib Sat Mar 21 22:12:21 2020 +0100
@@ -2204,8 +2204,8 @@
booktitle = {Intelligent Computer Mathematics (CICM 2019)},
year = {2019},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Sacerdoti Coen, Claudio},
- volume = {????},
- series = LNAI,
+ volume = {11617},
+ series = "LNAI",
publisher = {Springer},
note = {\url{https://arxiv.org/abs/1905.01735}}
}
--- a/src/Pure/PIDE/rendering.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Sat Mar 21 22:12:21 2020 +0100
@@ -209,7 +209,7 @@
Markup.BAD)
val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
- val error_elements = Markup.Elements(Markup.ERROR, Markup.BAD)
+ val error_elements = Markup.Elements(Markup.ERROR)
val caret_focus_elements = Markup.Elements(Markup.ENTITY)
--- a/src/Pure/System/isabelle_system.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Mar 21 22:12:21 2020 +0100
@@ -170,7 +170,7 @@
/* tmp files */
- private def isabelle_tmp_prefix(): JFile =
+ def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
path.file.mkdirs // low-level mkdirs
--- a/src/Pure/Thy/sessions.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Mar 21 22:12:21 2020 +0100
@@ -222,7 +222,7 @@
val required_sessions =
dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory))
.map(theory => imports_base.theory_qualifier(theory))
- .filterNot(_ == info.name)
+ .filter(name => name != info.name && sessions_structure.defined(name))
val required_subgraph =
sessions_structure.imports_graph
@@ -386,6 +386,8 @@
if (required_theories.isEmpty) (ancestor.get, Nil)
else {
val other_name = info.name + "_requirements(" + ancestor.get + ")"
+ Isabelle_System.isabelle_tmp_prefix()
+
(other_name,
List(
make_info(info.options,
--- a/src/Pure/Tools/build.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/build.scala Sat Mar 21 22:12:21 2020 +0100
@@ -294,7 +294,6 @@
}
process.result(
- progress_stderr = Output.writeln(_),
progress_stdout = (line: String) =>
Library.try_unprefix("\floading_theory = ", line) match {
case Some(theory) =>
--- a/src/Pure/Tools/build_docker.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/build_docker.scala Sat Mar 21 22:12:21 2020 +0100
@@ -67,7 +67,8 @@
mv """ + isabelle_name + """ Isabelle && \
perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
- Isabelle/bin/isabelle build -o system_heaps -b """ + logic +
+ Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
+ rm Isabelle.tar.gz""" +
(if (entrypoint) """
ENTRYPOINT ["Isabelle/bin/isabelle"]
@@ -128,13 +129,6 @@
Build Isabelle docker image with default logic image, using a standard
Isabelle application archive for Linux (local file or remote URL).
-
- Examples:
-
- isabelle build_docker -E -t test/isabelle:Isabelle2019 Isabelle2019_linux.tar.gz
-
- isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2019_linux.tar.gz
-
""",
"B:" -> (arg => base = arg),
"E" -> (_ => entrypoint = true),
--- a/src/Pure/Tools/dump.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/dump.scala Sat Mar 21 22:12:21 2020 +0100
@@ -98,7 +98,8 @@
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
- pure_base: Boolean = false): Context =
+ pure_base: Boolean = false,
+ skip_base: Boolean = false): Context =
{
val session_options: Options =
{
@@ -125,7 +126,7 @@
val deps: Sessions.Deps =
Sessions.deps(sessions_structure, progress = progress).check_errors
- new Context(options, progress, dirs, select_dirs, pure_base, session_options, deps)
+ new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps)
}
}
@@ -135,6 +136,7 @@
val dirs: List[Path],
val select_dirs: List[Path],
val pure_base: Boolean,
+ val skip_base: Boolean,
val session_options: Options,
val deps: Sessions.Deps)
{
@@ -189,7 +191,7 @@
val PURE = isabelle.Thy_Header.PURE
val base =
- if (logic == PURE && !pure_base) Nil
+ if ((logic == PURE && !pure_base) || skip_base) Nil
else make_session(base_sessions, session_logic = PURE, strict = logic == PURE)
val main =
--- a/src/Pure/Tools/update.scala Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/Tools/update.scala Sat Mar 21 22:12:21 2020 +0100
@@ -18,7 +18,7 @@
{
val context =
Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
- selection = selection)
+ selection = selection, skip_base = true)
context.build_logic(logic)
--- a/src/Pure/thm_deps.ML Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Pure/thm_deps.ML Sat Mar 21 22:12:21 2020 +0100
@@ -42,7 +42,11 @@
fun prt_oracle (ora, NONE) = prt_ora ora
| prt_oracle (ora, SOME prop) =
prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
- in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;
+ val oracles =
+ (case try all_oracles thms of
+ SOME oracles => oracles
+ | NONE => error "Malformed proofs")
+ in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) oracles) end;
(* thm_deps *)
@@ -70,8 +74,12 @@
fun pretty_thm_deps thy thms =
let
val ctxt = Proof_Context.init_global thy;
+ val deps =
+ (case try (thm_deps thy) thms of
+ SOME deps => deps
+ | NONE => error "Malformed proofs");
val items =
- map #2 (thm_deps thy thms)
+ map #2 deps
|> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
|> sort_by (#2 o #1)
|> map (fn ((marks, xname), i) =>
--- a/src/Tools/jEdit/src/jEdit.props Thu Mar 19 11:57:43 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Sat Mar 21 22:12:21 2020 +0100
@@ -321,7 +321,7 @@
vfs.favorite.4=isabelle-export:
vfs.favorite.5.type=1
vfs.favorite.5=isabelle-session:
-view.antiAlias=standard
+view.antiAlias=subpixel HRGB
view.blockCaret=true
view.caretBlink=false
view.docking.framework=PIDE
--- a/src/ZF/Constructible/AC_in_L.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Sat Mar 21 22:12:21 2020 +0100
@@ -460,7 +460,7 @@
apply (blast dest!: well_ord_L_r intro: well_ord_subset)
done
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
theorem "\<forall>x[L]. \<exists>r. wellordered(L,x,r)"
proof
@@ -469,7 +469,7 @@
then obtain r where "well_ord(x,r)"
by (blast dest: L_implies_AC)
thus "\<exists>r. wellordered(L,x,r)"
- by (blast intro: well_ord_imp_relativized)
+ by (blast intro: L.well_ord_imp_relativized)
qed
text\<open>In order to prove \<^term>\<open> \<exists>r[L]. wellordered(L,x,r)\<close>, it's necessary to know
--- a/src/ZF/Constructible/DPow_absolute.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Sat Mar 21 22:12:21 2020 +0100
@@ -581,7 +581,7 @@
==> transrec_replacement(L, \<lambda>x f u.
\<exists>r[L]. is_Replace(L, x, transrec_body(L,f,x), r) &
big_union(L, r, u), j)"
-apply (rule transrec_replacementI, assumption)
+apply (rule L.transrec_replacementI, assumption)
apply (unfold transrec_body_def)
apply (rule strong_replacementI)
apply (rule_tac u="{j,B,Memrel(eclose({j}))}"
--- a/src/ZF/Constructible/L_axioms.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Sat Mar 21 22:12:21 2020 +0100
@@ -110,7 +110,7 @@
apply (rule Union_ax)
done
-interpretation L?: M_trivial L by (rule M_trivial_L)
+interpretation L: M_trivial L by (rule M_trivial_L)
(* Replaces the following declarations...
lemmas rall_abs = M_trivial.rall_abs [OF M_trivial_L]
--- a/src/ZF/Constructible/Rec_Separation.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Sat Mar 21 22:12:21 2020 +0100
@@ -184,7 +184,7 @@
theorem M_trancl_L: "M_trancl(L)"
by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
-interpretation L?: M_trancl L by (rule M_trancl_L)
+interpretation L: M_trancl L by (rule M_trancl_L)
subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>list\<close>\<close>
@@ -371,7 +371,7 @@
apply (rule M_datatypes_axioms_L)
done
-interpretation L?: M_datatypes L by (rule M_datatypes_L)
+interpretation L: M_datatypes L by (rule M_datatypes_L)
subsection\<open>\<^term>\<open>L\<close> is Closed Under the Operator \<^term>\<open>eclose\<close>\<close>
@@ -434,7 +434,7 @@
apply (rule M_eclose_axioms_L)
done
-interpretation L?: M_eclose L by (rule M_eclose_L)
+interpretation L: M_eclose L by (rule M_eclose_L)
end
--- a/src/ZF/Constructible/Satisfies_absolute.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Sat Mar 21 22:12:21 2020 +0100
@@ -961,11 +961,11 @@
lemma formula_rec_replacement:
\<comment> \<open>For the \<^term>\<open>transrec\<close>\<close>
"[|n \<in> nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
-apply (rule transrec_replacementI, simp add: nat_into_M)
+apply (rule L.transrec_replacementI, simp add: L.nat_into_M)
apply (rule strong_replacementI)
apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
in gen_separation_multi [OF formula_rec_replacement_Reflects],
- auto simp add: nat_into_M)
+ auto simp add: L.nat_into_M)
apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
done
--- a/src/ZF/Constructible/Separation.thy Thu Mar 19 11:57:43 2020 +0100
+++ b/src/ZF/Constructible/Separation.thy Sat Mar 21 22:12:21 2020 +0100
@@ -304,7 +304,7 @@
theorem M_basic_L: " M_basic(L)"
by (rule M_basic.intro [OF M_trivial_L M_basic_axioms_L])
-interpretation L?: M_basic L by (rule M_basic_L)
+interpretation L: M_basic L by (rule M_basic_L)
end