# HG changeset patch
# User wenzelm
# Date 1526810237 -7200
# Node ID 1f7308050349bf6893e12467295e605235087bea
# Parent  88dd06301dd30f5fcf0435db1256749bc10bc5e8
prefer HTTPS;

diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/Implementation/ML.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/JEdit/JEdit.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/Locales/Examples3.thy
--- 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>
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/Main/Main_Doc.thy
--- 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}
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/Prog_Prove/Basics.thy
--- 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.
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/System/Misc.thy
--- 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.
diff -r 88dd06301dd3 -r 1f7308050349 src/Doc/System/Server.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Analysis/Continuous_Extension.thy
--- 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"
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Analysis/Gamma_Function.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Analysis/Linear_Algebra.thy
--- 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:
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Analysis/Weierstrass_Theorems.thy
--- 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"
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Factorial.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Imperative_HOL/Ref.thy
--- 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>
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Library/Open_State_Syntax.thy
--- 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>
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Nominal/Examples/CK_Machine.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- 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 =
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- 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>
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/String.thy
--- 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).
 
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Tools/ATP/atp_systems.ML
--- 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"
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Tools/sat_solver.ML
--- 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)                      *)
 (* ------------------------------------------------------------------------- *)
 
 (* ------------------------------------------------------------------------- *)
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/Types_To_Sets/Types_To_Sets.thy
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/ex/NatSum.thy
--- 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] =
diff -r 88dd06301dd3 -r 1f7308050349 src/HOL/ex/Sudoku.thy
--- 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>
 
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/Admin/build_jdk.scala
--- 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.
 
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/Admin/isabelle_devel.scala
--- 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(")"),
 
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/GUI/wrap_panel.scala
--- 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.
 */
 
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/General/utf8.scala
--- 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 =
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/Thy/bibtex.scala
--- 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
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/Tools/find_consts.ML
--- 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.
 *)
 
diff -r 88dd06301dd3 -r 1f7308050349 src/Pure/Tools/spell_checker.scala
--- 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