--- 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;
--- 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
--- 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
--- 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}}}
--- 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,
--- 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}
--- 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
--- 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}}}
--- 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\,}
--- 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}}}
--- 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}
--- 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
--- 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
--- 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},
--- 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\<open>Preliminaries\<close>
+subsection%unimportant \<open>Preliminaries\<close>
lemma sum_le_prod:
fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
@@ -54,17 +54,18 @@
subsection\<open>Definitions and basic properties\<close>
-definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
+definition%important raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool"
where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
-definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
+definition%important
+ has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"
-definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
+definition%important convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
"convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p"
-definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
+definition%important prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
(binder "\<Prod>" 10)
where "prodinf f = (THE p. f has_prod p)"
@@ -146,7 +147,7 @@
subsection\<open>Absolutely convergent products\<close>
-definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
+definition%important abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
"abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>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 \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
assumes "\<And>i. f i \<noteq> 0"
shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
@@ -367,7 +368,7 @@
qed
qed
-lemma abs_convergent_prod_conv_summable:
+theorem abs_convergent_prod_conv_summable:
fixes f :: "nat \<Rightarrow> 'a :: real_normed_div_algebra"
shows "abs_convergent_prod f \<longleftrightarrow> summable (\<lambda>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 \<open>Ignoring initial segments\<close>
+
lemma convergent_prod_offset:
assumes "convergent_prod (\<lambda>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\<open>Ignoring initial segments\<close>
lemma raw_has_prod_ignore_initial_segment:
fixes f :: "nat \<Rightarrow> '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 \<Rightarrow> 'a :: real_normed_field"
assumes "convergent_prod f"
shows "convergent_prod (\<lambda>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 \<Rightarrow> 'a :: real_normed_field"
assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
shows "\<exists>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 (\<lambda>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\<open>More elementary properties\<close>
+
+theorem abs_convergent_prod_imp_convergent_prod:
fixes f :: "nat \<Rightarrow> '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\<open>More elementary properties\<close>
-
lemma raw_has_prod_cases:
fixes f :: "nat \<Rightarrow> '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 \<Rightarrow> 'a::{semidom,t2_space}"
assumes "\<And>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 \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
+theorem has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
proof
assume "f has_prod x"
then show "convergent_prod f \<and> prodinf f = x"
@@ -871,7 +873,7 @@
end
-subsection \<open>Infinite products on ordered, topological monoids\<close>
+subsection%unimportant \<open>Infinite products on ordered topological monoids\<close>
lemma LIMSEQ_prod_0:
fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}"
@@ -1072,7 +1074,7 @@
using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
-subsection \<open>Infinite products on topological spaces\<close>
+subsection%unimportant \<open>Infinite products on topological spaces\<close>
context
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
@@ -1173,7 +1175,7 @@
end
-subsection \<open>Infinite summability on real normed fields\<close>
+subsection%unimportant \<open>Infinite summability on real normed fields\<close>
context
fixes f :: "nat \<Rightarrow> '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 "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0"
shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> 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 \<Rightarrow> real"
assumes "\<And>n. a n > 0"
shows "convergent_prod (\<lambda>k. 1 + a k) \<longleftrightarrow> 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 \<Rightarrow> complex"
assumes z: "\<And>j. z j \<noteq> 0" and \<xi>: "\<xi> \<noteq> 0"
shows "((\<lambda>n. \<Prod>j\<le>n. z j) \<longlonglongrightarrow> \<xi>) \<longleftrightarrow> (\<exists>k. (\<lambda>n. (\<Sum>j\<le>n. Ln (z j))) \<longlonglongrightarrow> Ln \<xi> + of_int k * (of_real(2*pi) * \<i>))" (is "?lhs = ?rhs")
@@ -1769,7 +1771,7 @@
using convergent_prod_def assms convergent_prod_iff_summable_complex by blast
-subsection\<open>Embeddings from the reals into some complete real normed field\<close>
+subsection%unimportant \<open>Embeddings from the reals into some complete real normed field\<close>
lemma tendsto_eq_of_real_lim:
assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
--- 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 \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
(infix "abs'_summable'_on" 50)
where
"f abs_summable_on A \<longleftrightarrow> integrable (count_space A) f"
-definition infsetsum ::
+definition%important infsetsum ::
"('a \<Rightarrow> 'b :: {banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> '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 (\<lambda>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 \<Rightarrow> 'b set"
assumes [simp]: "countable A" and "\<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 "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
shows "f abs_summable_on Sigma A B \<longleftrightarrow>
(\<forall>x\<in>A. (\<lambda>y. f (x, y)) abs_summable_on B x) \<and>
@@ -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 \<Rightarrow> 'b \<Rightarrow> 'c :: {real_normed_field,banach,second_countable_topology}"
assumes finite: "finite A" and countable: "\<And>x. x \<in> A \<Longrightarrow> countable (B x)"
assumes summable: "\<And>x. x \<in> A \<Longrightarrow> f x abs_summable_on B x"
--- 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\<open>Janiszewski's theorem\<close>
@@ -114,8 +113,8 @@
theorem Janiszewski:
- fixes a b::complex
- assumes "compact S" "closed T" and conST: "connected(S \<inter> T)"
+ fixes a b :: complex
+ assumes "compact S" "closed T" and conST: "connected (S \<inter> T)"
and ccS: "connected_component (- S) a b" and ccT: "connected_component (- T) a b"
shows "connected_component (- (S \<union> T)) a b"
proof -
@@ -166,6 +165,7 @@
using Janiszewski [OF ST]
by (metis IntD1 IntD2 notST compl_sup connected_iff_connected_component)
+
subsection\<open>The Jordan Curve theorem\<close>
lemma exists_double_arc:
@@ -219,7 +219,7 @@
qed
-theorem Jordan_curve:
+theorem%unimportant Jordan_curve:
fixes c :: "real \<Rightarrow> 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 \<Rightarrow> complex"
assumes "simple_path c" "pathfinish c = pathstart c"
shows "\<not> connected(- path_image c)"
--- 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,
--- 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.
--- 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}}
}
--- 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}
}
--- 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}
--- 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
--- 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,
--- 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")