summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sun, 20 May 2018 11:57:17 +0200 | |

changeset 68224 | 1f7308050349 |

parent 68223 | 88dd06301dd3 |

child 68225 | 2ce51f708ad6 |

prefer HTTPS;

--- 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