--- a/src/Doc/Implementation/ML.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/Implementation/ML.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/Locales/Examples3.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/Main/Main_Doc.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/System/Misc.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Doc/System/Server.thy Sun May 20 11:57:17 2018 +0200
@@ -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/HOL/Analysis/Continuous_Extension.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Continuous_Extension.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Factorial.thy Sun May 20 11:57:17 2018 +0200
@@ -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/Imperative_HOL/Ref.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Library/Open_State_Syntax.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/String.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Tools/sat_solver.ML Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy Sun May 20 11:57:17 2018 +0200
@@ -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/ex/NatSum.thy Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/ex/NatSum.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/HOL/ex/Sudoku.thy Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/Admin/build_jdk.scala Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala Sun May 20 11:57:17 2018 +0200
@@ -40,7 +40,7 @@
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(")"),
--- a/src/Pure/GUI/wrap_panel.scala Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/GUI/wrap_panel.scala Sun May 20 11:57:17 2018 +0200
@@ -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/utf8.scala Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/General/utf8.scala Sun May 20 11:57:17 2018 +0200
@@ -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/Thy/bibtex.scala Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/Thy/bibtex.scala Sun May 20 11:57:17 2018 +0200
@@ -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/Tools/find_consts.ML Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/Tools/find_consts.ML Sun May 20 11:57:17 2018 +0200
@@ -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 Sat May 19 20:42:34 2018 +0200
+++ b/src/Pure/Tools/spell_checker.scala Sun May 20 11:57:17 2018 +0200
@@ -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