prefer HTTPS;
authorwenzelm
Sun May 20 11:57:17 2018 +0200 (12 months ago)
changeset 682241f7308050349
parent 68223 88dd06301dd3
child 68225 2ce51f708ad6
prefer HTTPS;
src/Doc/Implementation/ML.thy
src/Doc/JEdit/JEdit.thy
src/Doc/Locales/Examples3.thy
src/Doc/Main/Main_Doc.thy
src/Doc/Prog_Prove/Basics.thy
src/Doc/System/Misc.thy
src/Doc/System/Server.thy
src/HOL/Analysis/Continuous_Extension.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Factorial.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Library/Open_State_Syntax.thy
src/HOL/Nominal/Examples/CK_Machine.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/String.thy
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/sat_solver.ML
src/HOL/Types_To_Sets/Types_To_Sets.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Sudoku.thy
src/Pure/Admin/build_jdk.scala
src/Pure/Admin/isabelle_devel.scala
src/Pure/GUI/wrap_panel.scala
src/Pure/General/utf8.scala
src/Pure/Thy/bibtex.scala
src/Pure/Tools/find_consts.ML
src/Pure/Tools/spell_checker.scala
     1.1 --- a/src/Doc/Implementation/ML.thy	Sat May 19 20:42:34 2018 +0200
     1.2 +++ b/src/Doc/Implementation/ML.thy	Sun May 20 11:57:17 2018 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    really going on and how things really work. This is a non-trivial aim, but
     1.5    it is supported by a certain style of writing Isabelle/ML that has emerged
     1.6    from long years of system development.\<^footnote>\<open>See also the interesting style guide
     1.7 -  for OCaml \<^url>\<open>http://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
     1.8 +  for OCaml \<^url>\<open>https://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
     1.9    which shares many of our means and ends.\<close>
    1.10  
    1.11    The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sat May 19 20:42:34 2018 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun May 20 11:57:17 2018 +0200
     2.3 @@ -38,9 +38,9 @@
     2.4      rich formal markup for GUI rendering.
     2.5  
     2.6      \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
     2.7 -    implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
     2.8 +    implemented in Java\<^footnote>\<open>\<^url>\<open>https://www.java.com\<close>\<close>. It is easily extensible by
     2.9      plugins written in any language that works on the JVM. In the context of
    2.10 -    Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
    2.11 +    Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.
    2.12  
    2.13      \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
    2.14      default user-interface for Isabelle. It targets both beginners and
    2.15 @@ -290,7 +290,7 @@
    2.16    The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
    2.17    Isabelle/jEdit. This is only relevant for building from sources, which also
    2.18    requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
    2.19 -  \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
    2.20 +  \<^url>\<open>https://isabelle.in.tum.de/components\<close>. The official Isabelle release
    2.21    already includes a pre-built version of Isabelle/jEdit.
    2.22  
    2.23    \<^bigskip>
    2.24 @@ -1925,7 +1925,7 @@
    2.25  chapter \<open>ML debugging within the Prover IDE\<close>
    2.26  
    2.27  text \<open>
    2.28 -  Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
    2.29 +  Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>https://www.polyml.org\<close>\<close> and thus
    2.30    benefits from the source-level debugger of that implementation of Standard
    2.31    ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
    2.32    ML threads, inspect the stack frame with local ML bindings, and evaluate ML
     3.1 --- a/src/Doc/Locales/Examples3.thy	Sat May 19 20:42:34 2018 +0200
     3.2 +++ b/src/Doc/Locales/Examples3.thy	Sun May 20 11:57:17 2018 +0200
     3.3 @@ -525,7 +525,7 @@
     3.4  
     3.5    The sources of this tutorial, which include all proofs, are
     3.6    available with the Isabelle distribution at
     3.7 -  \<^url>\<open>http://isabelle.in.tum.de\<close>.
     3.8 +  \<^url>\<open>https://isabelle.in.tum.de\<close>.
     3.9  \<close>
    3.10  
    3.11  text \<open>
     4.1 --- a/src/Doc/Main/Main_Doc.thy	Sat May 19 20:42:34 2018 +0200
     4.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun May 20 11:57:17 2018 +0200
     4.3 @@ -18,7 +18,7 @@
     4.4  text\<open>
     4.5  
     4.6  \begin{abstract}
     4.7 -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>.
     4.8 +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>.
     4.9  \end{abstract}
    4.10  
    4.11  \section*{HOL}
     5.1 --- a/src/Doc/Prog_Prove/Basics.thy	Sat May 19 20:42:34 2018 +0200
     5.2 +++ b/src/Doc/Prog_Prove/Basics.thy	Sun May 20 11:57:17 2018 +0200
     5.3 @@ -124,7 +124,7 @@
     5.4  \end{warn}
     5.5  
     5.6  In addition to the theories that come with the Isabelle/HOL distribution
     5.7 -(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
     5.8 +(see \<^url>\<open>https://isabelle.in.tum.de/library/HOL\<close>)
     5.9  there is also the \emph{Archive of Formal Proofs}
    5.10  at \<^url>\<open>https://isa-afp.org\<close>, a growing collection of Isabelle theories
    5.11  that everybody can contribute to.
     6.1 --- a/src/Doc/System/Misc.thy	Sat May 19 20:42:34 2018 +0200
     6.2 +++ b/src/Doc/System/Misc.thy	Sun May 20 11:57:17 2018 +0200
     6.3 @@ -29,13 +29,13 @@
     6.4    Resolve Isabelle components via download and installation.
     6.5    COMPONENTS are identified via base name.
     6.6  
     6.7 -  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>}
     6.8 +  ISABELLE_COMPONENT_REPOSITORY="https://isabelle.in.tum.de/components"\<close>}
     6.9  
    6.10    Components are initialized as described in \secref{sec:components} in a
    6.11    permissive manner, which can mark components as ``missing''. This state is
    6.12    amended by letting @{tool "components"} download and unpack components that
    6.13    are published on the default component repository
    6.14 -  \<^url>\<open>http://isabelle.in.tum.de/components\<close> in particular.
    6.15 +  \<^url>\<open>https://isabelle.in.tum.de/components\<close> in particular.
    6.16  
    6.17    Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
    6.18    \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
     7.1 --- a/src/Doc/System/Server.thy	Sat May 19 20:42:34 2018 +0200
     7.2 +++ b/src/Doc/System/Server.thy	Sun May 20 11:57:17 2018 +0200
     7.3 @@ -216,7 +216,7 @@
     7.4    Messages are read and written as byte streams (with byte lengths), but the
     7.5    content is always interpreted as plain text in terms of the UTF-8
     7.6    encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto''
     7.7 -  \<^url>\<open>http://utf8everywhere.org\<close>.\<close>
     7.8 +  \<^url>\<open>https://utf8everywhere.org\<close>.\<close>
     7.9  
    7.10    Note that line-endings and other formatting characters are invariant wrt.
    7.11    UTF-8 representation of text: thus implementations are free to determine the
     8.1 --- a/src/HOL/Analysis/Continuous_Extension.thy	Sat May 19 20:42:34 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Continuous_Extension.thy	Sun May 20 11:57:17 2018 +0200
     8.3 @@ -298,7 +298,7 @@
     8.4  subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
     8.5  
     8.6  text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
     8.7 -http://projecteuclid.org/euclid.pjm/1103052106\<close>
     8.8 +https://projecteuclid.org/euclid.pjm/1103052106\<close>
     8.9  
    8.10  theorem%important Dugundji:
    8.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
     9.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Sat May 19 20:42:34 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Sun May 20 11:57:17 2018 +0200
     9.3 @@ -335,7 +335,7 @@
     9.4    We now show that the log-Gamma series converges locally uniformly for all complex numbers except
     9.5    the non-positive integers. We do this by proving that the series is locally Cauchy, adapting this
     9.6    proof:
     9.7 -  http://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
     9.8 +  https://math.stackexchange.com/questions/887158/convergence-of-gammaz-lim-n-to-infty-fracnzn-prod-m-0nzm
     9.9  \<close>
    9.10  
    9.11  context
    10.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat May 19 20:42:34 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun May 20 11:57:17 2018 +0200
    10.3 @@ -283,7 +283,7 @@
    10.4  
    10.5  text \<open>TODO: The following lemmas about adjoints should hold for any
    10.6    Hilbert space (i.e. complete inner product space).
    10.7 -  (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
    10.8 +  (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
    10.9  \<close>
   10.10  
   10.11  lemma adjoint_works:
    11.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Sat May 19 20:42:34 2018 +0200
    11.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Sun May 20 11:57:17 2018 +0200
    11.3 @@ -174,7 +174,7 @@
    11.4  An Elementary Proof of the Stone-Weierstrass Theorem.
    11.5  Proceedings of the American Mathematical Society
    11.6  Volume 81, Number 1, January 1981.
    11.7 -DOI: 10.2307/2043993  http://www.jstor.org/stable/2043993\<close>
    11.8 +DOI: 10.2307/2043993  https://www.jstor.org/stable/2043993\<close>
    11.9  
   11.10  locale function_ring_on =
   11.11    fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
    12.1 --- a/src/HOL/Factorial.thy	Sat May 19 20:42:34 2018 +0200
    12.2 +++ b/src/HOL/Factorial.thy	Sun May 20 11:57:17 2018 +0200
    12.3 @@ -182,7 +182,7 @@
    12.4  
    12.5  subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
    12.6  
    12.7 -text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
    12.8 +text \<open>See \<^url>\<open>https://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
    12.9  
   12.10  context comm_semiring_1
   12.11  begin
    13.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Sat May 19 20:42:34 2018 +0200
    13.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Sun May 20 11:57:17 2018 +0200
    13.3 @@ -10,8 +10,8 @@
    13.4  
    13.5  text \<open>
    13.6    Imperative reference operations; modeled after their ML counterparts.
    13.7 -  See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
    13.8 -  and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
    13.9 +  See \<^url>\<open>https://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
   13.10 +  and \<^url>\<open>https://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
   13.11  \<close>
   13.12  
   13.13  subsection \<open>Primitives\<close>
    14.1 --- a/src/HOL/Library/Open_State_Syntax.thy	Sat May 19 20:42:34 2018 +0200
    14.2 +++ b/src/HOL/Library/Open_State_Syntax.thy	Sun May 20 11:57:17 2018 +0200
    14.3 @@ -20,7 +20,7 @@
    14.4    monads}, since a state is transformed single-threadedly).
    14.5  
    14.6    To enter from the Haskell world,
    14.7 -  \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
    14.8 +  \<^url>\<open>https://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
    14.9    a good motivating start.  Here we just sketch briefly how those
   14.10    monads enter the game of Isabelle/HOL.
   14.11  \<close>
    15.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Sat May 19 20:42:34 2018 +0200
    15.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Sun May 20 11:57:17 2018 +0200
    15.3 @@ -17,7 +17,7 @@
    15.4    written by Andy Pitts for his semantics course. See
    15.5    
    15.6       \<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close>
    15.7 -     \<^url>\<open>http://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
    15.8 +     \<^url>\<open>https://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
    15.9  \<close>
   15.10  
   15.11  atom_decl name
    16.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sat May 19 20:42:34 2018 +0200
    16.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun May 20 11:57:17 2018 +0200
    16.3 @@ -8,7 +8,7 @@
    16.4  
    16.5  text \<open>
    16.6    The proof is based on Gauss's fifth proof, which can be found at
    16.7 -  \<^url>\<open>http://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>.
    16.8 +  \<^url>\<open>https://www.lehigh.edu/~shw2/q-recip/gauss5.pdf\<close>.
    16.9  \<close>
   16.10  
   16.11  locale QR =
    17.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Sat May 19 20:42:34 2018 +0200
    17.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Sun May 20 11:57:17 2018 +0200
    17.3 @@ -4,7 +4,7 @@
    17.4    "HOL-Library.Code_Prolog"
    17.5  begin
    17.6  
    17.7 -text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
    17.8 +text \<open>An example from the experiments from SmallCheck (\<^url>\<open>https://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
    17.9  text \<open>The example (original in Haskell) was imported with Haskabelle and
   17.10    manually slightly adapted.
   17.11  \<close>
    18.1 --- a/src/HOL/String.thy	Sat May 19 20:42:34 2018 +0200
    18.2 +++ b/src/HOL/String.thy	Sun May 20 11:57:17 2018 +0200
    18.3 @@ -10,7 +10,7 @@
    18.4  
    18.5  text \<open>
    18.6    When modelling strings, we follow the approach given
    18.7 -  in @{url "http://utf8everywhere.org/"}:
    18.8 +  in @{url "https://utf8everywhere.org/"}:
    18.9  
   18.10    \<^item> Strings are a list of bytes (8 bit).
   18.11  
    19.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sat May 19 20:42:34 2018 +0200
    19.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 20 11:57:17 2018 +0200
    19.3 @@ -521,7 +521,7 @@
    19.4  
    19.5  val vampire_basic_options = "--proof tptp --output_axiom_names on --mode casc"
    19.6  
    19.7 -(* cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
    19.8 +(* cf. p. 20 of https://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
    19.9  val vampire_full_proof_options =
   19.10    " --forced_options splitting=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:\
   19.11    \naming=0"
    20.1 --- a/src/HOL/Tools/sat_solver.ML	Sat May 19 20:42:34 2018 +0200
    20.2 +++ b/src/HOL/Tools/sat_solver.ML	Sun May 20 11:57:17 2018 +0200
    20.3 @@ -825,7 +825,7 @@
    20.4  end;
    20.5  
    20.6  (* ------------------------------------------------------------------------- *)
    20.7 -(* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
    20.8 +(* zChaff (https://www.princeton.edu/~chaff/zchaff.html)                      *)
    20.9  (* ------------------------------------------------------------------------- *)
   20.10  
   20.11  (* ------------------------------------------------------------------------- *)
    21.1 --- a/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sat May 19 20:42:34 2018 +0200
    21.2 +++ b/src/HOL/Types_To_Sets/Types_To_Sets.thy	Sun May 20 11:57:17 2018 +0200
    21.3 @@ -7,7 +7,7 @@
    21.4  text \<open>This theory extends Isabelle/HOL's logic by two new inference rules
    21.5    to allow translation of types to sets as described in
    21.6    O. KunĨar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic
    21.7 -  available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
    21.8 +  available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close>
    21.9  
   21.10  theory Types_To_Sets
   21.11    imports Main
    22.1 --- a/src/HOL/ex/NatSum.thy	Sat May 19 20:42:34 2018 +0200
    22.2 +++ b/src/HOL/ex/NatSum.thy	Sun May 20 11:57:17 2018 +0200
    22.3 @@ -12,7 +12,7 @@
    22.4    Summing natural numbers, squares, cubes, etc.
    22.5  
    22.6    Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    22.7 -  \<^url>\<open>http://oeis.org\<close>.
    22.8 +  \<^url>\<open>https://oeis.org\<close>.
    22.9  \<close>
   22.10  
   22.11  lemmas [simp] =
    23.1 --- a/src/HOL/ex/Sudoku.thy	Sat May 19 20:42:34 2018 +0200
    23.2 +++ b/src/HOL/ex/Sudoku.thy	Sun May 20 11:57:17 2018 +0200
    23.3 @@ -136,7 +136,7 @@
    23.4  
    23.5  text \<open>
    23.6    Some ``exceptionally difficult'' Sudokus, taken from
    23.7 -  \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
    23.8 +  \<^url>\<open>https://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
    23.9    (accessed December~2, 2008).
   23.10  \<close>
   23.11  
    24.1 --- a/src/Pure/Admin/build_jdk.scala	Sat May 19 20:42:34 2018 +0200
    24.2 +++ b/src/Pure/Admin/build_jdk.scala	Sun May 20 11:57:17 2018 +0200
    24.3 @@ -57,7 +57,7 @@
    24.4    def readme(version: Version): String =
    24.5  """This is JDK/JRE """ + version.full + """ as required for Isabelle.
    24.6  
    24.7 -See http://www.oracle.com/technetwork/java/javase/downloads/index.html
    24.8 +See https://www.oracle.com/technetwork/java/javase/downloads/index.html
    24.9  for the original downloads, which are covered by the Oracle Binary
   24.10  Code License Agreement for Java SE.
   24.11  
    25.1 --- a/src/Pure/Admin/isabelle_devel.scala	Sat May 19 20:42:34 2018 +0200
    25.2 +++ b/src/Pure/Admin/isabelle_devel.scala	Sun May 20 11:57:17 2018 +0200
    25.3 @@ -40,7 +40,7 @@
    25.4              HTML.text("Database with recent ") :::
    25.5              List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
    25.6              HTML.text(" information (e.g. for ") :::
    25.7 -            List(HTML.link("http://sqlitebrowser.org",
    25.8 +            List(HTML.link("https://sqlitebrowser.org",
    25.9                List(HTML.code(HTML.text("sqlitebrowser"))))) :::
   25.10              HTML.text(")"),
   25.11  
    26.1 --- a/src/Pure/GUI/wrap_panel.scala	Sat May 19 20:42:34 2018 +0200
    26.2 +++ b/src/Pure/GUI/wrap_panel.scala	Sun May 20 11:57:17 2018 +0200
    26.3 @@ -3,7 +3,7 @@
    26.4  
    26.5  Panel with improved FlowLayout for wrapping of components over
    26.6  multiple lines, see also
    26.7 -http://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
    26.8 +https://tips4java.wordpress.com/2008/11/06/wrap-layout/ and
    26.9  scala.swing.FlowPanel.
   26.10  */
   26.11  
    27.1 --- a/src/Pure/General/utf8.scala	Sat May 19 20:42:34 2018 +0200
    27.2 +++ b/src/Pure/General/utf8.scala	Sun May 20 11:57:17 2018 +0200
    27.3 @@ -24,7 +24,7 @@
    27.4  
    27.5    /* permissive UTF-8 decoding */
    27.6  
    27.7 -  // see also http://en.wikipedia.org/wiki/UTF-8#Description
    27.8 +  // see also https://en.wikipedia.org/wiki/UTF-8#Description
    27.9    // overlong encodings enable byte-stuffing of low-ASCII
   27.10  
   27.11    def decode_permissive(text: CharSequence): String =
    28.1 --- a/src/Pure/Thy/bibtex.scala	Sat May 19 20:42:34 2018 +0200
    28.2 +++ b/src/Pure/Thy/bibtex.scala	Sun May 20 11:57:17 2018 +0200
    28.3 @@ -402,7 +402,7 @@
    28.4    private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
    28.5  
    28.6  
    28.7 -  // See also http://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
    28.8 +  // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
    28.9    // module @<Scan for and process a \.{.bib} command or database entry@>.
   28.10  
   28.11    object Parsers extends RegexParsers
    29.1 --- a/src/Pure/Tools/find_consts.ML	Sat May 19 20:42:34 2018 +0200
    29.2 +++ b/src/Pure/Tools/find_consts.ML	Sun May 20 11:57:17 2018 +0200
    29.3 @@ -1,7 +1,7 @@
    29.4  (*  Title:      Pure/Tools/find_consts.ML
    29.5      Author:     Timothy Bourke and Gerwin Klein, NICTA
    29.6  
    29.7 -Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
    29.8 +Hoogle-like (https://www-users.cs.york.ac.uk/~ndm/hoogle) searching by
    29.9  type over constants, but matching is not fuzzy.
   29.10  *)
   29.11  
    30.1 --- a/src/Pure/Tools/spell_checker.scala	Sat May 19 20:42:34 2018 +0200
    30.2 +++ b/src/Pure/Tools/spell_checker.scala	Sun May 20 11:57:17 2018 +0200
    30.3 @@ -2,7 +2,7 @@
    30.4      Author:     Makarius
    30.5  
    30.6  Spell checker with completion, based on JOrtho (see
    30.7 -http://sourceforge.net/projects/jortho).
    30.8 +https://sourceforge.net/projects/jortho).
    30.9  */
   30.10  
   30.11  package isabelle