--- a/Admin/components/components.sha1 Sun May 20 22:10:21 2018 +0100
+++ b/Admin/components/components.sha1 Sun May 20 22:10:30 2018 +0100
@@ -205,6 +205,7 @@
d66796a68ec3254b46b17b1f8ee5bcc56a93aacf scala-2.12.3.tar.gz
1636556167dff2c191baf502c23f12e09181ef78 scala-2.12.4.tar.gz
8171f494bba54fb0d01c887f889ab8fde7171c2a scala-2.12.5.tar.gz
+54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Sun May 20 22:10:21 2018 +0100
+++ b/Admin/components/main Sun May 20 22:10:30 2018 +0100
@@ -13,7 +13,7 @@
nunchaku-0.5
polyml-5.7.1-5
postgresql-42.2.2
-scala-2.12.5
+scala-2.12.6
smbc-0.4.1
ssh-java-20161009
spass-3.8ds-1
--- a/src/Doc/Implementation/ML.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Implementation/ML.thy Sun May 20 22:10:30 2018 +0100
@@ -38,7 +38,7 @@
really going on and how things really work. This is a non-trivial aim, but
it is supported by a certain style of writing Isabelle/ML that has emerged
from long years of system development.\<^footnote>\<open>See also the interesting style guide
- for OCaml \<^url>\<open>http://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
+ for OCaml \<^url>\<open>https://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
which shares many of our means and ends.\<close>
The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
--- a/src/Doc/JEdit/JEdit.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy Sun May 20 22:10:30 2018 +0100
@@ -38,9 +38,9 @@
rich formal markup for GUI rendering.
\<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
- implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
+ implemented in Java\<^footnote>\<open>\<^url>\<open>https://www.java.com\<close>\<close>. It is easily extensible by
plugins written in any language that works on the JVM. In the context of
- Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
+ Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.
\<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
default user-interface for Isabelle. It targets both beginners and
@@ -290,7 +290,7 @@
The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
Isabelle/jEdit. This is only relevant for building from sources, which also
requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
- \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
+ \<^url>\<open>https://isabelle.in.tum.de/components\<close>. The official Isabelle release
already includes a pre-built version of Isabelle/jEdit.
\<^bigskip>
@@ -1925,7 +1925,7 @@
chapter \<open>ML debugging within the Prover IDE\<close>
text \<open>
- Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
+ Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>https://www.polyml.org\<close>\<close> and thus
benefits from the source-level debugger of that implementation of Standard
ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
ML threads, inspect the stack frame with local ML bindings, and evaluate ML
--- a/src/Doc/Locales/Examples3.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Locales/Examples3.thy Sun May 20 22:10:30 2018 +0100
@@ -525,7 +525,7 @@
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
- \<^url>\<open>http://isabelle.in.tum.de\<close>.
+ \<^url>\<open>https://isabelle.in.tum.de\<close>.
\<close>
text \<open>
--- a/src/Doc/Main/Main_Doc.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy Sun May 20 22:10:30 2018 +0100
@@ -18,7 +18,7 @@
text\<open>
\begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>https://isabelle.in.tum.de/library/HOL\<close>.
\end{abstract}
\section*{HOL}
--- a/src/Doc/Prog_Prove/Basics.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Sun May 20 22:10:30 2018 +0100
@@ -124,7 +124,7 @@
\end{warn}
In addition to the theories that come with the Isabelle/HOL distribution
-(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
+(see \<^url>\<open>https://isabelle.in.tum.de/library/HOL\<close>)
there is also the \emph{Archive of Formal Proofs}
at \<^url>\<open>https://isa-afp.org\<close>, a growing collection of Isabelle theories
that everybody can contribute to.
--- a/src/Doc/System/Misc.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/System/Misc.thy Sun May 20 22:10:30 2018 +0100
@@ -29,13 +29,13 @@
Resolve Isabelle components via download and installation.
COMPONENTS are identified via base name.
- ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>}
+ ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>}
Components are initialized as described in \secref{sec:components} in a
permissive manner, which can mark components as ``missing''. This state is
amended by letting @{tool "components"} download and unpack components that
are published on the default component repository
- \<^url>\<open>http://isabelle.in.tum.de/components\<close> in particular.
+ \<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular.
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
--- a/src/Doc/System/Server.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/System/Server.thy Sun May 20 22:10:30 2018 +0100
@@ -216,7 +216,7 @@
Messages are read and written as byte streams (with byte lengths), but the
content is always interpreted as plain text in terms of the UTF-8
encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto''
- \<^url>\<open>http://utf8everywhere.org\<close>.\<close>
+ \<^url>\<open>https://utf8everywhere.org\<close>.\<close>
Note that line-endings and other formatting characters are invariant wrt.
UTF-8 representation of text: thus implementations are free to determine the
--- a/src/Doc/Tutorial/Protocol/Message.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Sun May 20 22:10:30 2018 +0100
@@ -785,8 +785,6 @@
lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
insert_commute [of "Key K" "Nonce N"]
- insert_commute [of "Key K" "Number N"]
- insert_commute [of "Key K" "Hash X"]
insert_commute [of "Key K" "MPair X Y"]
insert_commute [of "Key K" "Crypt X K'"]
for K C N X Y K'
@@ -795,8 +793,6 @@
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Nonce N"]
- insert_commute [of "Crypt X K" "Number N"]
- insert_commute [of "Crypt X K" "Hash X'"]
insert_commute [of "Crypt X K" "MPair X' Y"]
for X K C N X' Y
--- a/src/Doc/Tutorial/Rules/Forward.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/Doc/Tutorial/Rules/Forward.thy Sun May 20 22:10:30 2018 +0100
@@ -55,14 +55,14 @@
\<close>
-lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]
+lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k
lemmas gcd_mult_1 = gcd_mult_0 [simplified]
lemmas where1 = gcd_mult_distrib2 [where m=1]
lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1]
-lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"]
+lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k
text \<open>
example using ``of'':
@@ -87,7 +87,7 @@
lemmas gcd_mult0 = gcd_mult_1 [THEN sym]
(*not quite right: we need ?k but this gives k*)
-lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym]
+lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k
(*better in one step!*)
text \<open>
@@ -98,7 +98,7 @@
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym])
-lemmas gcd_self0 = gcd_mult [of k 1, simplified]
+lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k
text \<open>
--- a/src/HOL/Analysis/Continuous_Extension.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Analysis/Continuous_Extension.thy Sun May 20 22:10:30 2018 +0100
@@ -298,7 +298,7 @@
subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
-http://projecteuclid.org/euclid.pjm/1103052106\<close>
+https://projecteuclid.org/euclid.pjm/1103052106\<close>
theorem%important Dugundji:
fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
--- a/src/HOL/Analysis/Gamma_Function.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Sun May 20 22:10:30 2018 +0100
@@ -335,7 +335,7 @@
We now show that the log-Gamma series converges locally uniformly for all complex numbers except
the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this
proof:
- http://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
+ https://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
\<close>
context
--- a/src/HOL/Analysis/Linear_Algebra.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun May 20 22:10:30 2018 +0100
@@ -283,7 +283,7 @@
text \<open>TODO: The following lemmas about adjoints should hold for any
Hilbert space (i.e. complete inner product space).
- (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
+ (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
\<close>
lemma adjoint_works:
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Sun May 20 22:10:30 2018 +0100
@@ -174,7 +174,7 @@
An Elementary Proof of the Stone-Weierstrass Theorem.
Proceedings of the American Mathematical Society
Volume 81, Number 1, January 1981.
-DOI: 10.2307/2043993 http://www.jstor.org/stable/2043993\<close>
+DOI: 10.2307/2043993 https://www.jstor.org/stable/2043993\<close>
locale function_ring_on =
fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
--- a/src/HOL/Factorial.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Factorial.thy Sun May 20 22:10:30 2018 +0100
@@ -182,7 +182,7 @@
subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
-text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
+text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
context comm_semiring_1
begin
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sun May 20 22:10:30 2018 +0100
@@ -518,7 +518,7 @@
fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
let
val thm =
- Drule.zero_var_indexes
+ Drule.export_without_context
(@{thm lub_ID_reach} OF [chain_take, lub_take])
in
add_qualified_thm "reach" (dbind, thm) thy
@@ -551,7 +551,7 @@
else
let
fun prove_take_induct (chain_take, lub_take) =
- Drule.zero_var_indexes
+ Drule.export_without_context
(@{thm lub_ID_take_induct} OF [chain_take, lub_take])
val take_inducts =
map prove_take_induct (chain_take_thms ~~ lub_take_thms)
--- a/src/HOL/Imperative_HOL/Ref.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Imperative_HOL/Ref.thy Sun May 20 22:10:30 2018 +0100
@@ -10,8 +10,8 @@
text \<open>
Imperative reference operations; modeled after their ML counterparts.
- See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
- and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
+ See \<^url>\<open>https://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
+ and \<^url>\<open>https://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
\<close>
subsection \<open>Primitives\<close>
--- a/src/HOL/Library/Open_State_Syntax.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Library/Open_State_Syntax.thy Sun May 20 22:10:30 2018 +0100
@@ -20,7 +20,7 @@
monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
+ \<^url>\<open>https://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
a good motivating start. Here we just sketch briefly how those
monads enter the game of Isabelle/HOL.
\<close>
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Sun May 20 22:10:30 2018 +0100
@@ -17,7 +17,7 @@
written by Andy Pitts for his semantics course. See
\<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close>
- \<^url>\<open>http://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
+ \<^url>\<open>https://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
\<close>
atom_decl name
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun May 20 22:10:30 2018 +0100
@@ -8,7 +8,7 @@
text \<open>
The proof is based on Gauss's fifth proof, which can be found at
- \<^url>\<open>http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>.
+ \<^url>\<open>https://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>.
\<close>
locale QR =
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Sun May 20 22:10:30 2018 +0100
@@ -4,7 +4,7 @@
"HOL-Library.Code_Prolog"
begin
-text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
+text \<open>An example from the experiments from SmallCheck (\<^url>\<open>https://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
text \<open>The example (original in Haskell) was imported with Haskabelle and
manually slightly adapted.
\<close>
--- a/src/HOL/String.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/String.thy Sun May 20 22:10:30 2018 +0100
@@ -10,7 +10,7 @@
text \<open>
When modelling strings, we follow the approach given
- in @{url "http://utf8everywhere.org/"}:
+ in @{url "https://utf8everywhere.org/"}:
\<^item> Strings are a list of bytes (8 bit).
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 20 22:10:30 2018 +0100
@@ -521,7 +521,7 @@
val vampire_basic_options = "--proof tptp --output_axiom_names on --mode casc"
-(* cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
+(* cf. p. 20 of https://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
val vampire_full_proof_options =
" --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\
\naming=0"
--- a/src/HOL/Tools/sat_solver.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Tools/sat_solver.ML Sun May 20 22:10:30 2018 +0100
@@ -825,7 +825,7 @@
end;
(* ------------------------------------------------------------------------- *)
-(* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *)
+(* zChaff (https://www.princeton.edu/~chaff/zchaff.html) *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Types_To_Sets/Types_To_Sets.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Sun May 20 22:10:30 2018 +0100
@@ -7,7 +7,7 @@
text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
to allow translation of types to sets as described in
O. KunĨar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
- available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
+ available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
theory Types_To_Sets
imports Main
--- a/src/HOL/UNITY/Constrains.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/UNITY/Constrains.thy Sun May 20 22:10:30 2018 +0100
@@ -387,7 +387,7 @@
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always A"]
+lemmas Always_thin = thin_rl [of "F \<in> Always A"] for F A
subsection\<open>Totalize\<close>
--- a/src/HOL/ex/NatSum.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/ex/NatSum.thy Sun May 20 22:10:30 2018 +0100
@@ -12,7 +12,7 @@
Summing natural numbers, squares, cubes, etc.
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
- \<^url>\<open>http://oeis.org\<close>.
+ \<^url>\<open>https://oeis.org\<close>.
\<close>
lemmas [simp] =
--- a/src/HOL/ex/Sudoku.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/HOL/ex/Sudoku.thy Sun May 20 22:10:30 2018 +0100
@@ -136,7 +136,7 @@
text \<open>
Some ``exceptionally difficult'' Sudokus, taken from
- \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
+ \<^url>\<open>https://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
(accessed December~2, 2008).
\<close>
--- a/src/Pure/Admin/build_jdk.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Admin/build_jdk.scala Sun May 20 22:10:30 2018 +0100
@@ -57,7 +57,7 @@
def readme(version: Version): String =
"""This is JDK/JRE """ + version.full + """ as required for Isabelle.
-See http://www.oracle.com/technetwork/java/javase/downloads/index.html
+See https://www.oracle.com/technetwork/java/javase/downloads/index.html
for the original downloads, which are covered by the Oracle Binary
Code License Agreement for Java SE.
--- a/src/Pure/Admin/isabelle_devel.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Admin/isabelle_devel.scala Sun May 20 22:10:30 2018 +0100
@@ -33,6 +33,8 @@
List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
HTML.text(" (for all platforms)"),
+ HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file"))),
+
HTML.text("Isabelle ") :::
List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
HTML.text(" information"),
@@ -40,11 +42,9 @@
HTML.text("Database with recent ") :::
List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
HTML.text(" information (e.g. for ") :::
- List(HTML.link("http://sqlitebrowser.org",
+ List(HTML.link("https://sqlitebrowser.org",
List(HTML.code(HTML.text("sqlitebrowser"))))) :::
- HTML.text(")"),
-
- HTML.text("Cronjob ") ::: List(HTML.link(CRONJOB_LOG, HTML.text("log file")))))))
+ HTML.text(")")))))
}
--- a/src/Pure/GUI/wrap_panel.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/GUI/wrap_panel.scala Sun May 20 22:10:30 2018 +0100
@@ -3,7 +3,7 @@
Panel with improved FlowLayout for wrapping of components over
multiple lines, see also
-http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
+https://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
scala.swing.FlowPanel.
*/
--- a/src/Pure/General/buffer.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/General/buffer.ML Sun May 20 22:10:30 2018 +0100
@@ -11,6 +11,7 @@
val add: string -> T -> T
val markup: Markup.T -> (T -> T) -> T -> T
val content: T -> string
+ val chunks: T -> string list
val output: T -> BinIO.outstream -> unit
end;
@@ -30,7 +31,33 @@
fun content (Buffer xs) = implode (rev xs);
-fun output (Buffer xs) stream =
- List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (rev xs);
+
+(* chunks *)
+
+local
+
+val max_chunk = 4096;
+
+fun add_chunk [] res = res
+ | add_chunk chunk res = implode chunk :: res;
+
+fun rev_chunks [] _ chunk res = add_chunk chunk res
+ | rev_chunks (x :: xs) len chunk res =
+ let
+ val n = size x;
+ val len' = len + n;
+ in
+ if len' < max_chunk then rev_chunks xs len' (x :: chunk) res
+ else rev_chunks xs n [x] (add_chunk chunk res)
+ end;
+
+in
+
+fun chunks (Buffer xs) = rev_chunks xs 0 [] [];
+
+fun output buf stream =
+ List.app (fn s => BinIO.output (stream, Byte.stringToBytes s)) (chunks buf);
end;
+
+end;
--- a/src/Pure/General/url.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/General/url.ML Sun May 20 22:10:30 2018 +0100
@@ -9,6 +9,7 @@
datatype T =
File of Path.T |
Http of string * Path.T |
+ Https of string * Path.T |
Ftp of string * Path.T
val append: T -> T -> T
val implode: T -> string
@@ -25,6 +26,7 @@
datatype T =
File of Path.T |
Http of string * Path.T |
+ Https of string * Path.T |
Ftp of string * Path.T;
@@ -32,6 +34,7 @@
fun append (File p) (File p') = File (Path.append p p')
| append (Http (h, p)) (File p') = Http (h, Path.append p p')
+ | append (Https (h, p)) (File p') = Https (h, Path.append p p')
| append (Ftp (h, p)) (File p') = Ftp (h, Path.append p p')
| append _ url = url;
@@ -42,6 +45,7 @@
fun implode_url (File p) = implode_path p
| implode_url (Http (h, p)) = "http://" ^ h ^ implode_path p
+ | implode_url (Https (h, p)) = "https://" ^ h ^ implode_path p
| implode_url (Ftp (h, p)) = "ftp://" ^ h ^ implode_path p;
@@ -57,14 +61,16 @@
val scan_path_root = Scan.many Symbol.not_eof >> (Path.explode o implode o cons "/");
val scan_url =
- Scan.unless (Scan.this_string "file:" ||
- Scan.this_string "http:" || Scan.this_string "ftp:") scan_path >> File ||
+ Scan.unless
+ (Scan.this_string "file:" || Scan.this_string "http:" ||
+ Scan.this_string "https:" || Scan.this_string "ftp:") scan_path >> File ||
Scan.this_string "file:///" |-- scan_path_root >> File ||
Scan.this_string "file://localhost/" |-- scan_path_root >> File ||
Scan.this_string "file://" |-- scan_host -- scan_path
>> (fn (h, p) => File (Path.append (Path.named_root h) p)) ||
Scan.this_string "file:/" |-- scan_path_root >> File ||
Scan.this_string "http://" |-- scan_host -- scan_path >> Http ||
+ Scan.this_string "https://" |-- scan_host -- scan_path >> Https ||
Scan.this_string "ftp://" |-- scan_host -- scan_path >> Ftp;
in
--- a/src/Pure/General/utf8.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/General/utf8.scala Sun May 20 22:10:30 2018 +0100
@@ -24,7 +24,7 @@
/* permissive UTF-8 decoding */
- // see also http://en.wikipedia.org/wiki/UTF-8#Description
+ // see also https://en.wikipedia.org/wiki/UTF-8#Description
// overlong encodings enable byte-stuffing of low-ASCII
def decode_permissive(text: CharSequence): String =
--- a/src/Pure/PIDE/yxml.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/PIDE/yxml.ML Sun May 20 22:10:30 2018 +0100
@@ -21,6 +21,8 @@
val embed_controls: string -> string
val detect: string -> bool
val output_markup: Markup.T -> string * string
+ val buffer_body: XML.body -> Buffer.T -> Buffer.T
+ val buffer: XML.tree -> Buffer.T -> Buffer.T
val string_of_body: XML.body -> string
val string_of: XML.tree -> string
val output_markup_elem: Markup.T -> (string * string) * string
@@ -66,17 +68,17 @@
if Markup.is_empty markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
-fun string_of_body body =
- let
- fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
- fun tree (XML.Elem ((name, atts), ts)) =
- Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
- trees ts #>
- Buffer.add XYX
- | tree (XML.Text s) = Buffer.add s
- and trees ts = fold tree ts;
- in Buffer.empty |> trees body |> Buffer.content end;
+fun buffer_attrib (a, x) =
+ Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+fun buffer_body ts = fold buffer ts
+and buffer (XML.Elem ((name, atts), ts)) =
+ Buffer.add XY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add X #>
+ buffer_body ts #>
+ Buffer.add XYX
+ | buffer (XML.Text s) = Buffer.add s
+
+fun string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content;
val string_of = string_of_body o single;
--- a/src/Pure/Thy/bibtex.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala Sun May 20 22:10:30 2018 +0100
@@ -402,7 +402,7 @@
private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
- // See also http://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
+ // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
// module @<Scan for and process a \.{.bib} command or database entry@>.
object Parsers extends RegexParsers
--- a/src/Pure/Thy/export_theory.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML Sun May 20 22:10:30 2018 +0100
@@ -20,7 +20,7 @@
if Options.bool (#options context) "export_theory" then f context thy else ()));
fun export_body thy name body =
- Export.export thy ("theory/" ^ name) [YXML.string_of_body body];
+ Export.export thy ("theory/" ^ name) (Buffer.chunks (YXML.buffer_body body Buffer.empty));
(* presentation *)
@@ -32,8 +32,7 @@
val parents = Theory.parents_of thy;
val _ =
export_body thy "parents"
- let open XML.Encode
- in list string (map Context.theory_long_name parents) end;
+ (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
(* entities *)
@@ -98,22 +97,28 @@
(#constants (Consts.dest (Sign.consts_of thy)));
- (* axioms *)
+ (* axioms and facts *)
- val encode_axiom =
+ val encode_props =
let open XML.Encode Term_XML.Encode
- in triple (list (pair string sort)) (list (pair string typ)) term end;
+ in triple (list (pair string sort)) (list (pair string typ)) (list term) end;
- fun export_axiom prop =
+ fun export_props props =
let
- val prop' = Logic.unvarify_global prop;
- val typargs = rev (Term.add_tfrees prop' []);
- val args = rev (Term.add_frees prop' []);
- in encode_axiom (typargs, args, prop') end;
+ val props' = map Logic.unvarify_global props;
+ val typargs = rev (fold Term.add_tfrees props' []);
+ val args = rev (fold Term.add_frees props' []);
+ in encode_props (typargs, args, props') end;
+
+ val export_axiom = export_props o single;
+ val export_fact = export_props o Term_Subst.zero_var_indexes_list o map Thm.full_prop_of;
val _ =
export_entities "axioms" (K (SOME o export_axiom)) Theory.axiom_space
(Theory.axioms_of thy);
+ val _ =
+ export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
+ (Facts.dest_static true [] (Global_Theory.facts_of thy));
in () end);
--- a/src/Pure/Thy/export_theory.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala Sun May 20 22:10:30 2018 +0100
@@ -54,23 +54,23 @@
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
consts: List[Const],
- axioms: List[Axiom])
+ axioms: List[Axiom],
+ facts: List[Fact])
{
override def toString: String = name
}
- def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil)
+ def empty_theory(name: String): Theory = Theory(name, Nil, Nil, Nil, Nil, Nil)
def read_theory(db: SQL.Database, session_name: String, theory_name: String,
types: Boolean = true,
consts: Boolean = true,
- axioms: Boolean = true): Theory =
+ axioms: Boolean = true,
+ facts: Boolean = true): Theory =
{
val parents =
Export.read_entry(db, session_name, theory_name, "theory/parents") match {
- case Some(entry) =>
- import XML.Decode._
- list(string)(entry.uncompressed_yxml())
+ case Some(entry) => split_lines(entry.uncompressed().text)
case None =>
error("Missing theory export in session " + quote(session_name) + ": " +
quote(theory_name))
@@ -78,7 +78,8 @@
Theory(theory_name, parents,
if (types) read_types(db, session_name, theory_name) else Nil,
if (consts) read_consts(db, session_name, theory_name) else Nil,
- if (axioms) read_axioms(db, session_name, theory_name) else Nil)
+ if (axioms) read_axioms(db, session_name, theory_name) else Nil,
+ if (facts) read_facts(db, session_name, theory_name) else Nil)
}
@@ -150,7 +151,15 @@
})
- /* axioms */
+ /* axioms and facts */
+
+ def decode_props(body: XML.Body):
+ (List[(String, Term.Sort)], List[(String, Term.Typ)], List[Term.Term]) =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ triple(list(pair(string, sort)), list(pair(string, typ)), list(term))(body)
+ }
sealed case class Axiom(
entity: Entity,
@@ -163,12 +172,22 @@
(tree: XML.Tree) =>
{
val (entity, body) = decode_entity(tree)
- val (typargs, args, prop) =
- {
- import XML.Decode._
- import Term_XML.Decode._
- triple(list(pair(string, sort)), list(pair(string, typ)), term)(body)
- }
+ val (typargs, args, List(prop)) = decode_props(body)
Axiom(entity, typargs, args, prop)
})
+
+ sealed case class Fact(
+ entity: Entity,
+ typargs: List[(String, Term.Sort)],
+ args: List[(String, Term.Typ)],
+ props: List[Term.Term])
+
+ def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
+ read_entities(db, session_name, theory_name, "facts",
+ (tree: XML.Tree) =>
+ {
+ val (entity, body) = decode_entity(tree)
+ val (typargs, args, props) = decode_props(body)
+ Fact(entity, typargs, args, props)
+ })
}
--- a/src/Pure/Tools/build.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Tools/build.ML Sun May 20 22:10:30 2018 +0100
@@ -99,7 +99,7 @@
then
let
val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
- val _ = File.open_output (fn out => List.app (File.output out) output) path;
+ val _ = File.write_list path output;
in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
else
(case Markup.dest_loading_theory props of
--- a/src/Pure/Tools/find_consts.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Tools/find_consts.ML Sun May 20 22:10:30 2018 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Tools/find_consts.ML
Author: Timothy Bourke and Gerwin Klein, NICTA
-Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
+Hoogle-like (https://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
type over constants, but matching is not fuzzy.
*)
--- a/src/Pure/Tools/spell_checker.scala Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/Tools/spell_checker.scala Sun May 20 22:10:30 2018 +0100
@@ -2,7 +2,7 @@
Author: Makarius
Spell checker with completion, based on JOrtho (see
-http://sourceforge.net/projects/jortho).
+https://sourceforge.net/projects/jortho).
*/
package isabelle
--- a/src/Pure/term_subst.ML Sun May 20 22:10:21 2018 +0100
+++ b/src/Pure/term_subst.ML Sun May 20 22:10:30 2018 +0100
@@ -29,9 +29,10 @@
val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
term -> term
- val zero_var_indexes: term -> term
val zero_var_indexes_inst: term list ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list
+ val zero_var_indexes: term -> term
+ val zero_var_indexes_list: term list -> term list
end;
structure Term_Subst: TERM_SUBST =
@@ -224,6 +225,7 @@
([], Name.context);
in (instT, inst) end;
-fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;
+fun zero_var_indexes_list ts = map (instantiate (zero_var_indexes_inst ts)) ts;
+val zero_var_indexes = singleton zero_var_indexes_list;
end;
--- a/src/ZF/Bin.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/ZF/Bin.thy Sun May 20 22:10:30 2018 +0100
@@ -652,15 +652,6 @@
(** For cancel_numerals **)
-lemmas rel_iff_rel_0_rls =
- zless_iff_zdiff_zless_0 [where y = "u $+ v"]
- eq_iff_zdiff_eq_0 [where y = "u $+ v"]
- zle_iff_zdiff_zle_0 [where y = "u $+ v"]
- zless_iff_zdiff_zless_0 [where y = n]
- eq_iff_zdiff_eq_0 [where y = n]
- zle_iff_zdiff_zle_0 [where y = n]
- for u v (* FIXME n (!?) *)
-
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m = intify(n))"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
@@ -673,6 +664,18 @@
apply (simp add: zadd_ac)
done
+context fixes n :: i
+begin
+
+lemmas rel_iff_rel_0_rls =
+ zless_iff_zdiff_zless_0 [where y = "u $+ v"]
+ eq_iff_zdiff_eq_0 [where y = "u $+ v"]
+ zle_iff_zdiff_zle_0 [where y = "u $+ v"]
+ zless_iff_zdiff_zless_0 [where y = n]
+ eq_iff_zdiff_eq_0 [where y = n]
+ zle_iff_zdiff_zle_0 [where y = n]
+ for u v
+
lemma less_add_iff1: "(i$*u $+ m $< j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $< n)"
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
@@ -681,6 +684,8 @@
apply (simp add: zdiff_def zadd_zmult_distrib zadd_ac rel_iff_rel_0_rls)
done
+end
+
lemma le_add_iff1: "(i$*u $+ m $\<le> j$*u $+ n) \<longleftrightarrow> ((i$-j)$*u $+ m $\<le> n)"
apply (simp add: zdiff_def zadd_zmult_distrib)
apply (simp add: zcompare_rls)
--- a/src/ZF/Induct/Tree_Forest.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Sun May 20 22:10:30 2018 +0100
@@ -22,7 +22,7 @@
tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
and forest'induct =
tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
- for t
+ for t f
declare tree_forest.intros [simp, TC]
--- a/src/ZF/UNITY/Constrains.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/ZF/UNITY/Constrains.thy Sun May 20 22:10:30 2018 +0100
@@ -451,7 +451,7 @@
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
+lemmas Always_thin = thin_rl [of "F \<in> Always(A)"] for F A
(*To allow expansion of the program's definition when appropriate*)
named_theorems program "program definitions"
--- a/src/ZF/upair.thy Sun May 20 22:10:21 2018 +0100
+++ b/src/ZF/upair.thy Sun May 20 22:10:30 2018 +0100
@@ -230,10 +230,10 @@
**)
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
-lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
+lemmas split_if_eq2 = split_if [of "%x. a = x"] for a
lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
-lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
+lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2