# HG changeset patch # User traytel # Date 1531988552 -3600 # Node ID 5a5146c3a35b773d32266f09cd069c071ddb66cc # Parent 1e37b45ce3fbc6db823711492f18755a0f72e4c9# Parent 16d98ef49a2cadd8f6cfd75561c23a453cd0929a merged diff -r 1e37b45ce3fb -r 5a5146c3a35b Admin/components/README --- a/Admin/components/README Thu Jul 19 09:10:22 2018 +0100 +++ b/Admin/components/README Thu Jul 19 09:22:32 2018 +0100 @@ -38,7 +38,7 @@ Isabelle components are managed as authentic .tar.gz archives in /home/isabelle/components from where they are made publicly available -on http://isabelle.in.tum.de/components/. +on https://isabelle.in.tum.de/components/. Visibility on the HTTP server depends on local Unix file permission: nonfree components should omit "read" mode for the Unix group/other; diff -r 1e37b45ce3fb -r 5a5146c3a35b Admin/cronjob/self_update --- a/Admin/cronjob/self_update Thu Jul 19 09:10:22 2018 +0100 +++ b/Admin/cronjob/self_update Thu Jul 19 09:22:32 2018 +0100 @@ -11,7 +11,7 @@ mkdir -p run log { - hg -R isabelle pull "https://isabelle.in.tum.de/repos/isabelle" || echo "self_update pull failed" >&2 + hg -R isabelle pull "https://isabelle.sketis.net/repos/isabelle" || echo "self_update pull failed" >&2 hg -R isabelle update -C || echo "self_update update failed" >&2 isabelle/bin/isabelle components -a 2>&1 || echo "self_update components failed" >&2 } > run/self_update.out diff -r 1e37b45ce3fb -r 5a5146c3a35b README --- a/README Thu Jul 19 09:10:22 2018 +0100 +++ b/README Thu Jul 19 09:22:32 2018 +0100 @@ -34,10 +34,10 @@ The Isabelle home page may be accessed from the following mirror sites: - * http://www.cl.cam.ac.uk/research/hvg/Isabelle - * http://isabelle.in.tum.de + * https://www.cl.cam.ac.uk/research/hvg/Isabelle + * https://isabelle.in.tum.de * http://mirror.cse.unsw.edu.au/pub/isabelle - * http://mirror.clarkson.edu/isabelle + * https://mirror.clarkson.edu/isabelle Mailing list diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/How_to_Prove_it/document/root.bib --- a/src/Doc/How_to_Prove_it/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/How_to_Prove_it/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -3,12 +3,12 @@ @string{Springer="Springer-Verlag"} @manual{Main,author={Tobias Nipkow},title={What's in Main}, -note={\url{http://isabelle.in.tum.de/doc/main.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/main.pdf}}} @manual{ProgProve,author={Tobias Nipkow}, title={Programming and Proving in Isabelle/HOL}, -note={\url{http://isabelle.in.tum.de/doc/prog-prove.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/prog-prove.pdf}}} @manual{IsarRef,author={Makarius Wenzel}, title={The Isabelle/Isar Reference Manual}, -note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Locales/document/root.bib --- a/src/Doc/Locales/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Locales/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -1,7 +1,7 @@ @unpublished{IsarRef, author = "Markus Wenzel", title = "The {Isabelle/Isar} Reference Manual", - note = "Part of the Isabelle distribution, \url{http://isabelle.in.tum.de/doc/isar-ref.pdf}." + note = "Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}." } @book {Jacobson1985, diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Logics/document/preface.tex --- a/src/Doc/Logics/document/preface.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Logics/document/preface.tex Thu Jul 19 09:22:32 2018 +0100 @@ -56,7 +56,7 @@ \begin{center}\small \begin{tabular}{l} \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\ - \url{http://isabelle.in.tum.de/library/} \\ + \url{https://isabelle.in.tum.de/library/} \\ \end{tabular} \end{center} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Prog_Prove/document/intro-isabelle.tex --- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Thu Jul 19 09:22:32 2018 +0100 @@ -56,7 +56,7 @@ If you have not done so already, download and install Isabelle (this book is compatible with Isabelle2016-1) -from \url{http://isabelle.in.tum.de}. You can start it by clicking +from \url{https://isabelle.in.tum.de}. You can start it by clicking on the application icon. This will launch Isabelle's user interface based on the text editor \concept{jEdit}. Below you see a typical example snapshot of a session. At this point we merely explain diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Prog_Prove/document/root.bib --- a/src/Doc/Prog_Prove/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Prog_Prove/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -13,10 +13,10 @@ @manual{Krauss,author={Alexander Krauss}, title={Defining Recursive Functions in Isabelle/HOL}, -note={\url{http://isabelle.in.tum.de/doc/functions.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/functions.pdf}}} @manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main}, -note={\url{http://isabelle.in.tum.de/doc/main.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/main.pdf}}} @book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel}, title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic", @@ -28,4 +28,4 @@ @manual{IsarRef,author={Makarius Wenzel}, title={The Isabelle/Isar Reference Manual}, -note={\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}} +note={\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Jul 19 09:22:32 2018 +0100 @@ -13,7 +13,7 @@ %\usepackage[scaled=.85]{beramono} \usepackage{isabelle,iman,pdfsetup} -\newcommand\download{\url{http://isabelle.in.tum.de/components/}} +\newcommand\download{\url{https://isabelle.in.tum.de/components/}} \let\oldS=\S \def\S{\oldS\,} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Sugar/document/root.bib --- a/src/Doc/Sugar/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Sugar/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -8,5 +8,5 @@ @misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow}, title={{LaTeX} sugar theories and support files}, -note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}} +note={\url{https://isabelle.in.tum.de/sugar.tar.gz}}} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Tutorial/document/basics.tex --- a/src/Doc/Tutorial/document/basics.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Tutorial/document/basics.tex Thu Jul 19 09:22:32 2018 +0100 @@ -85,7 +85,7 @@ \end{warn} HOL's theory collection is available online at \begin{center}\small - \url{http://isabelle.in.tum.de/library/HOL/} + \url{https://isabelle.in.tum.de/library/HOL/} \end{center} and is recommended browsing. In subdirectory \texttt{Library} you find a growing library of useful theories that are not part of \isa{Main} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Tutorial/document/fp.tex --- a/src/Doc/Tutorial/document/fp.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Tutorial/document/fp.tex Thu Jul 19 09:22:32 2018 +0100 @@ -130,7 +130,7 @@ Lists are one of the essential datatypes in computing. We expect that you are already familiar with their basic operations. Theory \isa{ToyList} is only a small fragment of HOL's predefined theory -\thydx{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. +\thydx{List}\footnote{\url{https://isabelle.in.tum.de/library/HOL/List.html}}. The latter contains many further operations. For example, the functions \cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first element and the remainder of a list. (However, pattern matching is usually diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/Tutorial/document/preface.tex --- a/src/Doc/Tutorial/document/preface.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/Tutorial/document/preface.tex Thu Jul 19 09:22:32 2018 +0100 @@ -35,7 +35,7 @@ from output generated in this way. The final chapter of Part~I explains how users may produce their own formal documents in a similar fashion. -Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains +Isabelle's \hfootref{https://isabelle.in.tum.de/}{web site} contains links to the download area and to documentation and other information. The classic Isabelle user interface is Proof~General~/ Emacs by David Aspinall's\index{Aspinall, David}. This book says very little about diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Doc/manual.bib --- a/src/Doc/manual.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Doc/manual.bib Thu Jul 19 09:22:32 2018 +0100 @@ -158,7 +158,7 @@ author = {Clemens Ballarin}, title = {Tutorial to Locales and Locale Interpretation}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/locales.pdf}} } @article{Ballarin2014, @@ -226,7 +226,7 @@ Markus Wenzel}, title = {The Supplemental {Isabelle/HOL} Library}, note = {Part of the Isabelle distribution, - \url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, + \url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, year = 2002 } @@ -311,7 +311,7 @@ author = {Julian Biendarra and Jasmin Christian Blanchette and Martin Desharnais and Lorenz Panny and Andrei Popescu and Dmitriy Traytel}, title = {Defining (Co)datatypes and Primitively (Co)recursive Functions in {Isabelle\slash HOL}}, institution = {TU Munich}, - note = {\url{http://isabelle.in.tum.de/doc/datatypes.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/datatypes.pdf}}} @book{Bird-Wadler,author="Richard Bird and Philip Wadler", title="Introduction to Functional Programming",publisher=PH,year=1988} @@ -324,21 +324,21 @@ author = {Jasmin Christian Blanchette}, title = {Picking Nits: A User's Guide to {N}itpick for {I}sabelle\slash {HOL}}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/nitpick.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/nitpick.pdf}} } @manual{isabelle-sledgehammer, author = {Jasmin Christian Blanchette}, title = {Hammering Away: A User's Guide to {S}ledgehammer for {I}sabelle\slash {HOL}}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/sledgehammer.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/sledgehammer.pdf}} } @manual{isabelle-corec, author = {Jasmin Christian Blanchette and Andreas Lochbihler and Andrei Popescu and Dmitriy Traytel}, title = {Defining Nonprimitively Corecursive Functions in {Isabelle\slash HOL}}, institution = {TU Munich}, - note = {\url{http://isabelle.in.tum.de/doc/corec.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/corec.pdf}}} @inproceedings{blanchette-nipkow-2010, title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder", @@ -831,14 +831,14 @@ author = {Florian Haftmann}, title = {Haskell-style type classes with {Isabelle}/{Isar}}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/classes.pdf}} } @manual{isabelle-codegen, author = {Florian Haftmann}, title = {Code generation from Isabelle theories}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/codegen.pdf}} } @Book{halmos60, @@ -1064,7 +1064,7 @@ author = {Alexander Krauss}, title = {Defining Recursive Functions in {Isabelle/HOL}}, institution = TUM, - note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/functions.pdf}} } @inproceedings{Kuncar:2015, @@ -1366,7 +1366,7 @@ title = {{Isabelle}'s Logics: {HOL}}, institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t M{\"u}nchen and Computer Laboratory, University of Cambridge}, - note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}}} @article{nipkow-prehofer, author = {Tobias Nipkow and Christian Prehofer}, @@ -1502,25 +1502,25 @@ author = {Lawrence C. Paulson}, title = {Old Introduction to {Isabelle}}, institution = CUCL, - note = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/intro.pdf}}} @manual{isabelle-logics, author = {Lawrence C. Paulson}, title = {{Isabelle's} Logics}, institution = CUCL, - note = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/logics.pdf}}} @manual{isabelle-ref, author = {Lawrence C. Paulson}, title = {The Old {Isabelle} Reference Manual}, institution = CUCL, - note = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/ref.pdf}}} @manual{isabelle-ZF, author = {Lawrence C. Paulson}, title = {{Isabelle}'s Logics: {FOL} and {ZF}}, institution = CUCL, - note = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/logics-ZF.pdf}}} @article{paulson-found, author = {Lawrence C. Paulson}, @@ -2024,22 +2024,22 @@ @manual{isabelle-system, author = {Makarius Wenzel}, title = {The {Isabelle} System Manual}, - note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/system.pdf}}} @manual{isabelle-jedit, author = {Makarius Wenzel}, title = {{Isabelle/jEdit}}, - note = {\url{http://isabelle.in.tum.de/doc/jedit.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/jedit.pdf}}} @manual{isabelle-isar-ref, author = {Makarius Wenzel}, title = {The {Isabelle/Isar} Reference Manual}, - note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}}} @manual{isabelle-implementation, author = {Makarius Wenzel}, title = {The {Isabelle/Isar} Implementation}, - note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}} + note = {\url{https://isabelle.in.tum.de/doc/implementation.pdf}}} @InProceedings{Wenzel:1999:TPHOL, author = {Markus Wenzel}, diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/Analysis/Infinite_Products.thy --- a/src/HOL/Analysis/Infinite_Products.thy Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/Analysis/Infinite_Products.thy Thu Jul 19 09:22:32 2018 +0100 @@ -9,7 +9,7 @@ imports Topology_Euclidean_Space Complex_Transcendental begin -subsection\Preliminaries\ +subsection%unimportant \Preliminaries\ lemma sum_le_prod: fixes f :: "'a \ 'b :: linordered_semidom" @@ -54,17 +54,18 @@ subsection\Definitions and basic properties\ -definition raw_has_prod :: "[nat \ 'a::{t2_space, comm_semiring_1}, nat, 'a] \ bool" +definition%important raw_has_prod :: "[nat \ 'a::{t2_space, comm_semiring_1}, nat, 'a] \ bool" where "raw_has_prod f M p \ (\n. \i\n. f (i+M)) \ p \ p \ 0" text\The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\ -definition has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr "has'_prod" 80) +definition%important + has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr "has'_prod" 80) where "f has_prod p \ raw_has_prod f 0 p \ (\i q. p = 0 \ f i = 0 \ raw_has_prod f (Suc i) q)" -definition convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where +definition%important convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where "convergent_prod f \ \M p. raw_has_prod f M p" -definition prodinf :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a" +definition%important prodinf :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a" (binder "\" 10) where "prodinf f = (THE p. f has_prod p)" @@ -146,7 +147,7 @@ subsection\Absolutely convergent products\ -definition abs_convergent_prod :: "(nat \ _) \ bool" where +definition%important abs_convergent_prod :: "(nat \ _) \ bool" where "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))" lemma abs_convergent_prodI: @@ -220,7 +221,7 @@ by (rule_tac x=0 in exI) auto qed -lemma convergent_prod_iff_convergent: +lemma%important convergent_prod_iff_convergent: fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}" assumes "\i. f i \ 0" shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0" @@ -367,7 +368,7 @@ qed qed -lemma abs_convergent_prod_conv_summable: +theorem abs_convergent_prod_conv_summable: fixes f :: "nat \ 'a :: real_normed_div_algebra" shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))" by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) @@ -396,6 +397,8 @@ thus ?thesis by eventually_elim auto qed +subsection%unimportant \Ignoring initial segments\ + lemma convergent_prod_offset: assumes "convergent_prod (\n. f (n + m))" shows "convergent_prod f" @@ -411,7 +414,6 @@ shows "abs_convergent_prod f" using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) -subsection\Ignoring initial segments\ lemma raw_has_prod_ignore_initial_segment: fixes f :: "nat \ 'a :: real_normed_field" @@ -447,7 +449,7 @@ using raw_has_prod_def that by blast qed -corollary convergent_prod_ignore_initial_segment: +corollary%unimportant convergent_prod_ignore_initial_segment: fixes f :: "nat \ 'a :: real_normed_field" assumes "convergent_prod f" shows "convergent_prod (\n. f (n + m))" @@ -458,20 +460,22 @@ apply (auto simp add: raw_has_prod_def add_ac) done -corollary convergent_prod_ignore_nonzero_segment: +corollary%unimportant convergent_prod_ignore_nonzero_segment: fixes f :: "nat \ 'a :: real_normed_field" assumes f: "convergent_prod f" and nz: "\i. i \ M \ f i \ 0" shows "\p. raw_has_prod f M p" using convergent_prod_ignore_initial_segment [OF f] by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) -corollary abs_convergent_prod_ignore_initial_segment: +corollary%unimportant abs_convergent_prod_ignore_initial_segment: assumes "abs_convergent_prod f" shows "abs_convergent_prod (\n. f (n + m))" using assms unfolding abs_convergent_prod_def by (rule convergent_prod_ignore_initial_segment) -lemma abs_convergent_prod_imp_convergent_prod: +subsection\More elementary properties\ + +theorem abs_convergent_prod_imp_convergent_prod: fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" assumes "abs_convergent_prod f" shows "convergent_prod f" @@ -599,8 +603,6 @@ with L show ?thesis by (auto simp: prod_defs) qed -subsection\More elementary properties\ - lemma raw_has_prod_cases: fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}" assumes "raw_has_prod f M p" @@ -758,7 +760,7 @@ qed qed -corollary has_prod_0: +corollary%unimportant has_prod_0: fixes f :: "nat \ 'a::{semidom,t2_space}" assumes "\n. f n = 1" shows "f has_prod 1" @@ -851,7 +853,7 @@ by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le) -lemma has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x" +theorem has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x" proof assume "f has_prod x" then show "convergent_prod f \ prodinf f = x" @@ -871,7 +873,7 @@ end -subsection \Infinite products on ordered, topological monoids\ +subsection%unimportant \Infinite products on ordered topological monoids\ lemma LIMSEQ_prod_0: fixes f :: "nat \ 'a::{semidom,topological_space}" @@ -1072,7 +1074,7 @@ using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast -subsection \Infinite products on topological spaces\ +subsection%unimportant \Infinite products on topological spaces\ context fixes f g :: "nat \ 'a::{t2_space,topological_semigroup_mult,idom}" @@ -1173,7 +1175,7 @@ end -subsection \Infinite summability on real normed fields\ +subsection%unimportant \Infinite summability on real normed fields\ context fixes f :: "nat \ 'a::real_normed_field" @@ -1328,7 +1330,7 @@ by (simp add: ac_simps) qed -corollary has_prod_iff_shift': +corollary%unimportant has_prod_iff_shift': assumes "\i. i < n \ f i \ 0" shows "(\i. f (i + n)) has_prod (a / (\i f has_prod a" by (simp add: assms has_prod_iff_shift) @@ -1430,7 +1432,7 @@ end -lemma convergent_prod_iff_summable_real: +theorem convergent_prod_iff_summable_real: fixes a :: "nat \ real" assumes "\n. a n > 0" shows "convergent_prod (\k. 1 + a k) \ summable a" (is "?lhs = ?rhs") @@ -1556,7 +1558,7 @@ by (simp add: "0" f less_0_prodinf suminf_ln_real) -lemma Ln_prodinf_complex: +theorem Ln_prodinf_complex: fixes z :: "nat \ complex" assumes z: "\j. z j \ 0" and \: "\ \ 0" shows "((\n. \j\n. z j) \ \) \ (\k. (\n. (\j\n. Ln (z j))) \ Ln \ + of_int k * (of_real(2*pi) * \))" (is "?lhs = ?rhs") @@ -1769,7 +1771,7 @@ using convergent_prod_def assms convergent_prod_iff_summable_complex by blast -subsection\Embeddings from the reals into some complete real normed field\ +subsection%unimportant \Embeddings from the reals into some complete real normed field\ lemma tendsto_eq_of_real_lim: assumes "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \ q" diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/Analysis/Infinite_Set_Sum.thy --- a/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/Analysis/Infinite_Set_Sum.thy Thu Jul 19 09:22:32 2018 +0100 @@ -86,14 +86,14 @@ -definition abs_summable_on :: +definition%important abs_summable_on :: "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ bool" (infix "abs'_summable'_on" 50) where "f abs_summable_on A \ integrable (count_space A) f" -definition infsetsum :: +definition%important infsetsum :: "('a \ 'b :: {banach, second_countable_topology}) \ 'a set \ 'b" where "infsetsum f A = lebesgue_integral (count_space A) f" @@ -553,7 +553,7 @@ (insert assms, auto simp: bij_betw_def) qed -lemma infsetsum_reindex: +theorem infsetsum_reindex: assumes "inj_on g A" shows "infsetsum f (g ` A) = infsetsum (\x. f (g x)) A" by (intro infsetsum_reindex_bij_betw [symmetric] inj_on_imp_bij_betw assms) @@ -607,7 +607,7 @@ unfolding abs_summable_on_def infsetsum_def by (rule Bochner_Integration.integral_norm_bound) -lemma infsetsum_Sigma: +theorem infsetsum_Sigma: fixes A :: "'a set" and B :: "'a \ 'b set" assumes [simp]: "countable A" and "\i. countable (B i)" assumes summable: "f abs_summable_on (Sigma A B)" @@ -692,7 +692,7 @@ finally show ?thesis . qed -lemma abs_summable_on_Sigma_iff: +theorem abs_summable_on_Sigma_iff: assumes [simp]: "countable A" and "\x. x \ A \ countable (B x)" shows "f abs_summable_on Sigma A B \ (\x\A. (\y. f (x, y)) abs_summable_on B x) \ @@ -783,7 +783,7 @@ by (intro abs_summable_on_comparison_test' [OF abs_summable_on_Sigma_project1[OF assms]] norm_infsetsum_bound) -lemma infsetsum_prod_PiE: +theorem infsetsum_prod_PiE: fixes f :: "'a \ 'b \ 'c :: {real_normed_field,banach,second_countable_topology}" assumes finite: "finite A" and countable: "\x. x \ A \ countable (B x)" assumes summable: "\x. x \ A \ f x abs_summable_on B x" diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/Analysis/Jordan_Curve.thy --- a/src/HOL/Analysis/Jordan_Curve.thy Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/Analysis/Jordan_Curve.thy Thu Jul 19 09:22:32 2018 +0100 @@ -6,7 +6,6 @@ theory Jordan_Curve imports Arcwise_Connected Further_Topology - begin subsection\Janiszewski's theorem\ @@ -114,8 +113,8 @@ theorem Janiszewski: - fixes a b::complex - assumes "compact S" "closed T" and conST: "connected(S \ T)" + fixes a b :: complex + assumes "compact S" "closed T" and conST: "connected (S \ T)" and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b" shows "connected_component (- (S \ T)) a b" proof - @@ -166,6 +165,7 @@ using Janiszewski [OF ST] by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component) + subsection\The Jordan Curve theorem\ lemma exists_double_arc: @@ -219,7 +219,7 @@ qed -theorem Jordan_curve: +theorem%unimportant Jordan_curve: fixes c :: "real \ complex" assumes "simple_path c" and loop: "pathfinish c = pathstart c" obtains inner outer where @@ -389,7 +389,7 @@ qed -corollary Jordan_disconnected: +corollary%unimportant Jordan_disconnected: fixes c :: "real \ complex" assumes "simple_path c" "pathfinish c = pathstart c" shows "\ connected(- path_image c)" diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/Lattice/document/root.bib --- a/src/HOL/Lattice/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/Lattice/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -27,7 +27,7 @@ title = {Using Axiomatic Type Classes in Isabelle}, year = 2000, institution = {TU Munich}, - note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/axclass.pdf}} } @Manual{Wenzel:2000:isar-ref, @@ -35,7 +35,7 @@ title = {The {Isabelle/Isar} Reference Manual}, year = 2000, institution = {TU Munich}, - note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}} } @Proceedings{tphols99, diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/MicroJava/document/introduction.tex --- a/src/HOL/MicroJava/document/introduction.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/MicroJava/document/introduction.tex Thu Jul 19 09:22:32 2018 +0100 @@ -46,7 +46,7 @@ For a more complete Isabelle model of JavaCard, the reader should consult the Bali formalization -(\url{http://isabelle.in.tum.de/verificard/Bali/document.pdf}), which +(\url{https://isabelle.in.tum.de/verificard/Bali/document.pdf}), which models most of the source language features of JavaCard, however without describing the bytecode level. @@ -101,7 +101,7 @@ Initialization during object creation is not accounted for in the present document (see the formalization in -\url{http://isabelle.in.tum.de/verificard/obj-init/document.pdf}), +\url{https://isabelle.in.tum.de/verificard/obj-init/document.pdf}), neither is the \texttt{jsr} instruction. diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/MicroJava/document/root.bib --- a/src/HOL/MicroJava/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/MicroJava/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -20,7 +20,7 @@ embedding languages in theorem provers.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms = {Languages, Reliability, Theory, Verification}, - url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}}, + url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}}, pages = {117--144} } @@ -50,7 +50,7 @@ theorem prover Isabelle/HOL.}, CRClassification = {D.2.4, D.3.1, F.3.1}, CRGenTerms = {Languages, Verification, Theory}, - url = {\url{http://isabelle.in.tum.de/Bali/papers/ECOOP00.html}} + url = {\url{https://isabelle.in.tum.de/Bali/papers/ECOOP00.html}} } diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/NanoJava/document/root.bib --- a/src/HOL/NanoJava/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/NanoJava/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -12,7 +12,7 @@ and dynamic binding within method calls.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms = {Languages, Reliability, Theory, Verification}, - url = {\url{http://isabelle.in.tum.de/Bali/papers/NanoJava.html}}, + url = {\url{https://isabelle.in.tum.de/Bali/papers/NanoJava.html}}, note = {Submitted for publication.} } @@ -38,7 +38,7 @@ embedding languages in theorem provers.}, CRClassification = {D.3.1, F.3.2}, CRGenTerms = {Languages, Reliability, Theory, Verification}, - url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}}, + url = {\url{https://isabelle.in.tum.de/Bali/papers/MOD99.html}}, pages = {117--144} } @@ -74,5 +74,5 @@ but also gives maximal confidence in the results obtained.}, CRClassification = {D.2.4, D.3.1, F.3.1}, CRGenTerms = {Languages, Verification, Theory}, - note = {\url{http://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear} + note = {\url{https://isabelle.in.tum.de/Bali/papers/CPE01.html}, to appear} } diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/NanoJava/document/root.tex --- a/src/HOL/NanoJava/document/root.tex Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/NanoJava/document/root.tex Thu Jul 19 09:22:32 2018 +0100 @@ -36,7 +36,7 @@ implements a new approach for handling auxiliary variables. A more complex Hoare logic covering a much larger subset of Java is described in \cite{DvO-CPE01}.\\ -See also the homepage of project Bali at \url{http://isabelle.in.tum.de/Bali/} +See also the homepage of project Bali at \url{https://isabelle.in.tum.de/Bali/} and the conference version of this document \cite{NanoJava}. \end{abstract} diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/ROOT --- a/src/HOL/ROOT Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/ROOT Thu Jul 19 09:22:32 2018 +0100 @@ -188,7 +188,7 @@ This is an extension of IMP with local variables and mutually recursive procedures. For documentation see "Hoare Logic for Mutual Recursion and - Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). + Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). *} theories EvenOdd diff -r 1e37b45ce3fb -r 5a5146c3a35b src/HOL/Unix/document/root.bib --- a/src/HOL/Unix/document/root.bib Thu Jul 19 09:10:22 2018 +0100 +++ b/src/HOL/Unix/document/root.bib Thu Jul 19 09:22:32 2018 +0100 @@ -4,7 +4,7 @@ Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and Markus Wenzel}, title = {The Supplemental {Isabelle/HOL} Library}, - note = {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, + note = {\url{https://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, year = 2002 } @@ -21,7 +21,7 @@ institution = {Institut f\"ur Informatik, Technische Universi\"at M\"unchen and Computer Laboratory, University of Cambridge}, year = 2000, - note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/logics-HOL.pdf}} } @Book{Tanenbaum:1992, @@ -56,7 +56,7 @@ title = {The {Isabelle/Isar} Reference Manual}, year = 2002, institution = {TU Munich}, - note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}} + note = {\url{https://isabelle.in.tum.de/doc/isar-ref.pdf}} } @Proceedings{tphols99, diff -r 1e37b45ce3fb -r 5a5146c3a35b src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Thu Jul 19 09:10:22 2018 +0100 +++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Jul 19 09:22:32 2018 +0100 @@ -23,7 +23,7 @@ val current_log = main_dir + Path.explode("run/main.log") // owned by log service val cumulative_log = main_dir + Path.explode("log/main.log") // owned by log service - val isabelle_repos_source = "https://isabelle.in.tum.de/repos/isabelle" + val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle" val isabelle_repos = main_dir + Path.explode("isabelle") val afp_repos = main_dir + Path.explode("AFP")