Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorpaulson
Thu, 19 Jul 2018 17:28:13 +0200
changeset 68663 00a872706648
parent 68660 4ce18f389f53 (diff)
parent 68662 227f85b1b98c (current diff)
child 68664 bd0df72c16d5
merged
--- a/ANNOUNCE	Thu Jul 19 17:27:44 2018 +0200
+++ b/ANNOUNCE	Thu Jul 19 17:28:13 2018 +0200
@@ -20,6 +20,10 @@
 
 * Substantial additions to HOL-Analysis.
 
+* HOL-Library.Code_Lazy: code generation for lazy evaluation.
+
+* HOL-Real_Asymp: tools for semi-automatic real asymptotics.
+
 * Isabelle server for reactive communication with other programs.
 
 * More uniform 64-bit platform support: smaller Isabelle application.
--- a/Admin/components/README	Thu Jul 19 17:27:44 2018 +0200
+++ b/Admin/components/README	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/Admin/cronjob/self_update	Thu Jul 19 17:28:13 2018 +0200
@@ -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/NEWS	Thu Jul 19 17:27:44 2018 +0200
+++ b/NEWS	Thu Jul 19 17:28:13 2018 +0200
@@ -231,9 +231,6 @@
 
 *** HOL ***
 
-* New proof method "real_asymp" to prove asymptotics or real-valued 
-  functions (limits, "Big-O", etc.) automatically.
-
 * Sledgehammer: bundled version of "vampire" (for non-commercial users)
 helps to avoid fragility of "remote_vampire" service.
 
@@ -380,8 +377,8 @@
 * Theory HOL-Library.Code_Lazy provides a new preprocessor for the code
 generator to generate code for algebraic types with lazy evaluation
 semantics even in call-by-value target languages. See the theories
-HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for
-some examples.
+HOL-ex.Code_Lazy_Demo and HOL-Codegenerator_Test.Code_Lazy_Test for some
+examples.
 
 * Theory HOL-Library.Landau_Symbols has been moved here from AFP.
 
@@ -412,6 +409,9 @@
 Riemann mapping theorem, the Vitali covering theorem,
 change-of-variables results for integration and measures.
 
+* Session HOL-Real_Asymp: proof method "real_asymp" proves asymptotics
+or real-valued functions (limits, "Big-O", etc.) automatically.
+
 * Session HOL-Types_To_Sets: more tool support (unoverload_type combines
 internalize_sorts and unoverload) and larger experimental application
 (type based linear algebra transferred to linear algebra on subspaces).
--- a/README	Thu Jul 19 17:27:44 2018 +0200
+++ b/README	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/How_to_Prove_it/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Locales/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Logics/document/preface.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Prog_Prove/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Sugar/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Tutorial/document/basics.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Tutorial/document/fp.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/Tutorial/document/preface.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/Doc/manual.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Set_Sum.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -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/Cardinals/Cardinal_Arithmetic.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -8,7 +8,7 @@
 section \<open>Cardinal Arithmetic\<close>
 
 theory Cardinal_Arithmetic
-imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation
+imports Cardinal_Order_Relation
 begin
 
 subsection \<open>Binary sum\<close>
--- a/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Cardinals/Cardinal_Order_Relation.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -8,7 +8,7 @@
 section \<open>Cardinal-Order Relations\<close>
 
 theory Cardinal_Order_Relation
-imports HOL.BNF_Cardinal_Order_Relation Wellorder_Constructions
+imports Wellorder_Constructions
 begin
 
 declare
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -9,7 +9,7 @@
 
 theory Wellorder_Constructions
 imports
-  HOL.BNF_Wellorder_Constructions Wellorder_Embedding Order_Union
+  Wellorder_Embedding Order_Union
   "HOL-Library.Cardinal_Notations"
 begin
 
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -8,7 +8,7 @@
 section \<open>Well-Order Embeddings\<close>
 
 theory Wellorder_Embedding
-imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation
+imports Fun_More Wellorder_Relation
 begin
 
 subsection \<open>Auxiliaries\<close>
--- a/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Cardinals/Wellorder_Relation.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -8,7 +8,7 @@
 section \<open>Well-Order Relations\<close>
 
 theory Wellorder_Relation
-imports HOL.BNF_Wellorder_Relation Wellfounded_More
+imports Wellfounded_More
 begin
 
 context wo_rel
--- a/src/HOL/Lattice/document/root.bib	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Lattice/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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/Library/IArray.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Library/IArray.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -1,17 +1,21 @@
-section "Immutable Arrays with Code Generation"
+(*  Title:      HOL/Library/IArray.thy
+    Author:     Tobias Nipkow, TU Muenchen
+    Author:     Jose Divasón <jose.divasonm at unirioja.es>
+    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
+*)
+
+section \<open>Immutable Arrays with Code Generation\<close>
 
 theory IArray
 imports Main
 begin
 
-text\<open>Immutable arrays are lists wrapped up in an additional constructor.
+subsection \<open>Fundamental operations\<close>
+
+text \<open>Immutable arrays are lists wrapped up in an additional constructor.
 There are no update operations. Hence code generation can safely implement
 this type by efficient target language arrays.  Currently only SML is
-provided. Should be extended to other target languages and more operations.
-
-Note that arrays cannot be printed directly but only by turning them into
-lists first. Arrays could be converted back into lists for printing if they
-were wrapped up in an additional constructor.\<close>
+provided. Could be extended to other target languages and more operations.\<close>
 
 context
 begin
@@ -30,31 +34,23 @@
 qualified definition length :: "'a iarray \<Rightarrow> nat" where
 [simp]: "length as = List.length (IArray.list_of as)"
 
-qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"all p (IArray as) = (\<forall>a \<in> set as. p a)"
+qualified definition all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+[simp]: "all p as \<longleftrightarrow> (\<forall>a \<in> set (list_of as). p a)"
 
-qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"exists p (IArray as) = (\<exists>a \<in> set as. p a)"
+qualified definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+[simp]: "exists p as \<longleftrightarrow> (\<exists>a \<in> set (list_of as). p a)"
 
-lemma list_of_code [code]:
-"IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
-by (cases as) (simp add: map_nth)
+lemma of_fun_nth:
+"IArray.of_fun f n !! i = f i" if "i < n"
+using that by (simp add: map_nth)
 
 end
 
 
-subsection "Code Generation"
-
-code_reserved SML Vector
-
-code_printing
-  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
-| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
-| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
-| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
+subsection \<open>Generic code equations\<close>
 
 lemma [code]:
-  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
+  "size (as :: 'a iarray) = Suc (IArray.length as)"
   by (cases as) simp
 
 lemma [code]:
@@ -81,59 +77,17 @@
   "rel_iarray r as bs = list_all2 r (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) auto
 
+lemma list_of_code [code]:
+  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"
+  by (cases as) (simp add: map_nth)
+
 lemma [code]:
   "HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
   by (cases as, cases bs) (simp add: equal)
 
-context
-begin
-
-qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
-  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
-
-end
-
 lemma [code]:
-  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
-  by simp
-
-code_printing
-  constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
-
-context
-begin
-
-qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
-  [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
-
-end
-
-lemma [code]:
-  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
-  by simp
-
-lemma [code]:
-  "as !! n = IArray.sub' (as, integer_of_nat n)"
-  by simp
-
-code_printing
-  constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
-
-context
-begin
-
-qualified definition length' :: "'a iarray \<Rightarrow> integer" where
-  [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
-
-end
-
-lemma [code]:
-  "IArray.length' (IArray as) = integer_of_nat (List.length as)" 
-  by simp
-
-lemma [code]:
-  "IArray.length as = nat_of_integer (IArray.length' as)"
-  by simp
+  "IArray.all p = Not \<circ> IArray.exists (Not \<circ> p)"
+  by (simp add: fun_eq_iff)
 
 context term_syntax
 begin
@@ -145,7 +99,129 @@
 
 end
 
-code_printing
-  constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
+
+subsection \<open>Auxiliary operations for code generation\<close>
+
+context
+begin
+
+qualified primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
+  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
+
+lemma [code]:
+  "IArray.of_fun f n = IArray.tabulate (integer_of_nat n, f \<circ> nat_of_integer)"
+  by simp
+
+qualified primrec sub' :: "'a iarray \<times> integer \<Rightarrow> 'a" where
+  "sub' (as, n) = as !! nat_of_integer n"
+
+lemma [code]:
+  "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
+  by simp
+
+lemma [code]:
+  "as !! n = IArray.sub' (as, integer_of_nat n)"
+  by simp
+
+qualified definition length' :: "'a iarray \<Rightarrow> integer" where
+  [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
+
+lemma [code]:
+  "IArray.length' (IArray as) = integer_of_nat (List.length as)"
+  by simp
+
+lemma [code]:
+  "IArray.length as = nat_of_integer (IArray.length' as)"
+  by simp
+
+qualified definition exists_upto :: "('a \<Rightarrow> bool) \<Rightarrow> integer \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+  [simp]: "exists_upto p k as \<longleftrightarrow> (\<exists>l. 0 \<le> l \<and> l < k \<and> p (sub' (as, l)))"
+
+lemma exists_upto_of_nat:
+  "exists_upto p (of_nat n) as \<longleftrightarrow> (\<exists>m<n. p (as !! m))"
+  including integer.lifting by (simp, transfer)
+    (metis nat_int nat_less_iff of_nat_0_le_iff)
+
+lemma [code]:
+  "exists_upto p k as \<longleftrightarrow> (if k \<le> 0 then False else
+    let l = k - 1 in p (sub' (as, l)) \<or> exists_upto p l as)"
+proof (cases "k \<ge> 1")
+  case False
+  then show ?thesis
+    by (auto simp add: not_le discrete)
+next
+  case True
+  then have less: "k \<le> 0 \<longleftrightarrow> False"
+    by simp
+  define n where "n = nat_of_integer (k - 1)"
+  with True have k: "k - 1 = of_nat n" "k = of_nat (Suc n)"
+    by simp_all
+  show ?thesis unfolding less Let_def k(1) unfolding k(2) exists_upto_of_nat
+    using less_Suc_eq by auto
+qed
+
+lemma [code]:
+  "IArray.exists p as \<longleftrightarrow> exists_upto p (length' as) as"
+  including integer.lifting by (simp, transfer)
+   (auto, metis in_set_conv_nth less_imp_of_nat_less nat_int of_nat_0_le_iff)
 
 end
+
+
+subsection \<open>Code Generation for SML\<close>
+
+text \<open>Note that arrays cannot be printed directly but only by turning them into
+lists first. Arrays could be converted back into lists for printing if they
+were wrapped up in an additional constructor.\<close>
+
+code_reserved SML Vector
+
+code_printing
+  type_constructor iarray \<rightharpoonup> (SML) "_ Vector.vector"
+| constant IArray \<rightharpoonup> (SML) "Vector.fromList"
+| constant IArray.all \<rightharpoonup> (SML) "Vector.all"
+| constant IArray.exists \<rightharpoonup> (SML) "Vector.exists"
+| constant IArray.tabulate \<rightharpoonup> (SML) "Vector.tabulate"
+| constant IArray.sub' \<rightharpoonup> (SML) "Vector.sub"
+| constant IArray.length' \<rightharpoonup> (SML) "Vector.length"
+
+
+subsection \<open>Code Generation for Haskell\<close>
+
+text \<open>We map @{typ "'a iarray"}s in Isabelle/HOL to @{text Data.Array.IArray.array}
+  in Haskell.  Performance mapping to @{text Data.Array.Unboxed.Array} and
+  @{text Data.Array.Array} is similar.\<close>
+
+code_printing
+  code_module "IArray" \<rightharpoonup> (Haskell) \<open>
+  import Prelude (Bool(True, False), not, Maybe(Nothing, Just),
+    Integer, (+), (-), (<), fromInteger, toInteger, map, seq, (.));
+  import qualified Prelude;
+  import qualified Data.Array.IArray;
+  import qualified Data.Array.Base;
+  import qualified Data.Ix;
+
+  newtype IArray e = IArray (Data.Array.IArray.Array Integer e);
+
+  tabulate :: (Integer, (Integer -> e)) -> IArray e;
+  tabulate (k, f) = IArray (Data.Array.IArray.array (0, k - 1) (map (\i -> let fi = f i in fi `seq` (i, fi)) [0..k - 1]));
+
+  of_list :: [e] -> IArray e;
+  of_list l = IArray (Data.Array.IArray.listArray (0, (toInteger . Prelude.length) l - 1) l);
+
+  sub :: (IArray e, Integer) -> e;
+  sub (IArray v, i) = v `Data.Array.Base.unsafeAt` fromInteger i;
+
+  length :: IArray e -> Integer;
+  length (IArray v) = toInteger (Data.Ix.rangeSize (Data.Array.IArray.bounds v));\<close>
+
+code_reserved Haskell IArray_Impl
+
+code_printing
+  type_constructor iarray \<rightharpoonup> (Haskell) "IArray.IArray _"
+| constant IArray \<rightharpoonup> (Haskell) "IArray.of'_list"
+| constant IArray.tabulate \<rightharpoonup> (Haskell) "IArray.tabulate"
+| constant IArray.sub' \<rightharpoonup> (Haskell)  "IArray.sub"
+| constant IArray.length' \<rightharpoonup> (Haskell) "IArray.length"
+
+end
--- a/src/HOL/Library/Lattice_Syntax.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Library/Lattice_Syntax.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -3,7 +3,7 @@
 section \<open>Pretty syntax for lattice operations\<close>
 
 theory Lattice_Syntax
-imports HOL.Complete_Lattices
+imports Main
 begin
 
 notation
--- a/src/HOL/MicroJava/document/introduction.tex	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/MicroJava/document/introduction.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/MicroJava/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/NanoJava/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/NanoJava/document/root.tex	Thu Jul 19 17:28:13 2018 +0200
@@ -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/Quotient_Examples/Quotient_Int.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Quotient_Int
-imports "HOL-Library.Quotient_Product" HOL.Nat
+imports "HOL-Library.Quotient_Product"
 begin
 
 fun
--- a/src/HOL/ROOT	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/ROOT	Thu Jul 19 17:28:13 2018 +0200
@@ -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 17:27:44 2018 +0200
+++ b/src/HOL/Unix/document/root.bib	Thu Jul 19 17:28:13 2018 +0200
@@ -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/HOL/ex/Computations.thy	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/HOL/ex/Computations.thy	Thu Jul 19 17:28:13 2018 +0200
@@ -5,7 +5,7 @@
 section \<open>Simple example for computations generated by the code generator\<close>
 
 theory Computations
-  imports HOL.Nat HOL.Fun_Def HOL.Num HOL.Code_Numeral
+  imports Main
 begin
 
 fun even :: "nat \<Rightarrow> bool"
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Jul 19 17:27:44 2018 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Jul 19 17:28:13 2018 +0200
@@ -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")
isabelle