Loading theory "Integration.MonConv" (required by "Integration.Integral" via "Integration.RealRandVar" via "Integration.Measure")
Loading theory "Integration.Sigma_Algebra" (required by "Integration.Integral" via "Integration.RealRandVar" via "Integration.Measure")
Proofs for inductive predicate(s) "sigmap"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
overloading
  mon_conv_real \<equiv> mon_conv ::
    (nat \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool
  mon_conv_real_fun \<equiv> mon_conv ::
    (nat \<Rightarrow> 'a \<Rightarrow> real)
    \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool
  mon_conv_set \<equiv> mon_conv ::
    (nat \<Rightarrow> 'a set) \<Rightarrow> 'a set \<Rightarrow> bool
consts
  trivial_series ::
    "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
consts
  mk_mon ::
    "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set"
### theory "Integration.Sigma_Algebra"
### 0.332s elapsed time, 0.732s cpu time, 0.000s GC time
### theory "Integration.MonConv"
### 0.336s elapsed time, 0.740s cpu time, 0.000s GC time
Loading theory "Integration.Measure" (required by "Integration.Integral" via "Integration.RealRandVar")
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
consts
  mkdisjoint ::
    "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set"
consts
  trivial_series2 ::
    "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set"
### theory "Integration.Measure"
### 0.686s elapsed time, 1.248s cpu time, 0.000s GC time
Loading theory "Integration.RealRandVar" (required by "Integration.Integral")
### theory "Integration.RealRandVar"
### 0.761s elapsed time, 1.524s cpu time, 0.000s GC time
Loading theory "Integration.Failure"
Proofs for inductive predicate(s) "integral_setp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Integration.Failure"
### 0.463s elapsed time, 0.900s cpu time, 0.208s GC time
Loading theory "Integration.Integral"
Proofs for inductive predicate(s) "sfisp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "nnfisp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  mon_upclose_help ::
    "nat
     \<Rightarrow> (nat
                    \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> real)
                   \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> real"
### Ignoring duplicate rewrite rule:
### (0::?'a1) \<le> ?a1 \<Longrightarrow>
### (0::?'a1) \<le> ?a1 ^ ?n1 \<equiv> True
### Ambiguous input (line 2045 of "~~/afp/thys/Integration/Integral.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Integral.integral"
###       ("_lambda" ("_position" t)
###         ("\<^const>Groups.plus_class.plus"
###           ("_applC" ("_position" f) ("_position" t))
###           ("_applC" ("_position" g) ("_position" t))))
###       ("_position" M))
###     ("\<^const>Integral.integral" ("_position" f)
###       ("\<^const>Groups.plus_class.plus" ("_position" M)
###         ("\<^const>Integral.integral" ("_position" g) ("_position" M))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Integral.integral"
###       ("_lambda" ("_position" t)
###         ("\<^const>Groups.plus_class.plus"
###           ("_applC" ("_position" f) ("_position" t))
###           ("_applC" ("_position" g) ("_position" t))))
###       ("_position" M))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Integral.integral" ("_position" f) ("_position" M))
###       ("\<^const>Integral.integral" ("_position" g) ("_position" M)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 2228 of "~~/afp/thys/Integration/Integral.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("_applC" ("\<^const>RealRandVar.distribution")
###       ("_cargs" ("_position" M)
###         ("_cargs" ("_position" f)
###           ("\<^const>Set_Interval.ord_class.atLeast" ("_position" a)))))
###     ("\<^const>Integral.integral"
###       ("_lambda" ("_position" x)
###         ("\<^const>Power.power_class.power"
###           ("\<^const>Groups.abs_class.abs"
###             ("_applC" ("_position" f) ("_position" x)))
###           ("_position" n)))
###       ("\<^const>Fields.inverse_class.inverse_divide" ("_position" M)
###         ("\<^const>Power.power_class.power" ("_position" a)
###           ("_position" n))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Orderings.ord_class.less_eq"
###     ("_applC" ("\<^const>RealRandVar.distribution")
###       ("_cargs" ("_position" M)
###         ("_cargs" ("_position" f)
###           ("\<^const>Set_Interval.ord_class.atLeast" ("_position" a)))))
###     ("\<^const>Fields.inverse_class.inverse_divide"
###       ("\<^const>Integral.integral"
###         ("_lambda" ("_position" x)
###           ("\<^const>Power.power_class.power"
###             ("\<^const>Groups.abs_class.abs"
###               ("_applC" ("_position" f) ("_position" x)))
###             ("_position" n)))
###         ("_position" M))
###       ("\<^const>Power.power_class.power" ("_position" a)
###         ("_position" n)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "Integration.Integral"
### 0.685s elapsed time, 1.372s cpu time, 0.000s GC time
### Introduced fixed type variable(s): 'b in "t__"
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Ignoring duplicate rewrite rule:
### sum ?g1 {} \<equiv> 0::?'a1
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Ignoring duplicate rewrite rule:
### ((\<lambda>x. ?k1) \<longlongrightarrow> ?k1) ?F1 \<equiv> True
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
measure_space ?M \<Longrightarrow>
(?f \<in> rv ?M) = (\<forall>a. {w. a \<le> ?f w} \<in> measurable_sets ?M)
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
*** Failed to apply initial proof method (line 1828 of "~~/afp/thys/Integration/Integral.thy"):
*** using this:
***   \<forall>y. \<exists>N. \<forall>n\<ge>N. y < 2 ^ n
*** goal (1 subgoal):
***  1. (\<lambda>n. inverse (2 ^ n)) \<longlonglongrightarrow> 0
*** At command "by" (line 1828 of "~~/afp/thys/Integration/Integral.thy")
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Legacy feature! Old 'def' command -- use 'define' instead
### Ambiguous input (line 2092 of "~~/afp/thys/Integration/Integral.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Integral.integral"
###       ("_lambda" ("_position" t)
###         ("\<^const>Groups.plus_class.plus"
###           ("_applC" ("_position" f) ("_position" t))
###           ("_applC" ("_position" g) ("_position" t))))
###       ("_position" M))
###     ("\<^const>Integral.integral" ("_position" f)
###       ("\<^const>Groups.plus_class.plus" ("_position" M)
###         ("\<^const>Integral.integral" ("_position" g) ("_position" M))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>Integral.integral"
###       ("_lambda" ("_position" t)
###         ("\<^const>Groups.plus_class.plus"
###           ("_applC" ("_position" f) ("_position" t))
###           ("_applC" ("_position" g) ("_position" t))))
###       ("_position" M))
###     ("\<^const>Groups.plus_class.plus"
###       ("\<^const>Integral.integral" ("_position" f) ("_position" M))
###       ("\<^const>Integral.integral" ("_position" g) ("_position" M)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
isabelle document -c -o 'pdf' -n 'document' -t '' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Integration/document 2>&1
isabelle document -c -o 'pdf' -n 'outline' -t '/proof,/ML' /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Integration/outline 2>&1
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
No file root.aux.
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}]pdfTeX warning (ext4): destination with the s
ame identifier (name{page.1}) has been already used, duplicate ignored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably

LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 16.


LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 38.

[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex

LaTeX Warning: Reference `sec:measure-spaces' on page 4 undefined on input line
 29.


LaTeX Warning: Citation `hurd2002' on page 4 undefined on input line 30.

[4] [5]
Overfull \hbox (3.61127pt too wide) in paragraph at lines 401--414
[][]\OT1/cmr/bx/n/10 lemma as-sumes \OT1/cmr/m/it/10 s$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 sigma[]algebra a \OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 sigma[]alg
ebra[]UNIV$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 UNIV $\OMS/cmsy/m/n/10 2$ \OT1/c
mr/m/it/10 a$\OMS/cmsy/m/n/10 h[]i$[] 
) (./MonConv.tex

LaTeX Warning: Citation `Nipkow93' on page 6 undefined on input line 39.


LaTeX Warning: Citation `wenzelax' on page 6 undefined on input line 39.

[6]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 7 undefined on input line 9
7.

[7] [8]) (./Measure.tex

LaTeX Warning: Citation `hurd2002' on page 9 undefined on input line 28.

[9]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 10 undefined on input line 
79.


LaTeX Warning: Citation `Williams.mart' on page 10 undefined on input line 88.


LaTeX Warning: Citation `Bauer' on page 10 undefined on input line 107.

[10]

LaTeX Warning: Reference `nnfis' on page 11 undefined on input line 295.

) [11] (./RealRandVar.tex

LaTeX Warning: Citation `Skalberg' on page 12 undefined on input line 35.


LaTeX Warning: Reference `sec:measure-spaces' on page 12 undefined on input lin
e 42.


LaTeX Warning: Citation `mesfunc1' on page 12 undefined on input line 47.


LaTeX Warning: Citation `mesfunc2' on page 12 undefined on input line 47.


LaTeX Warning: Citation `hurd2002' on page 12 undefined on input line 56.

[12]

LaTeX Warning: Citation `Billingsley86' on page 13 undefined on input line 86.


LaTeX Warning: Citation `Bauer' on page 13 undefined on input line 88.


LaTeX Warning: Reference `sec:measure-spaces' on page 13 undefined on input lin
e 263.

[13]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 14 undefined on input line 
749.


Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[14] [15] [16]) [17]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 24.


LaTeX Warning: Citation `Bauer' on page 18 undefined on input line 25.


LaTeX Warning: Citation `Billingsley86' on page 18 undefined on input line 37.


LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 53.


LaTeX Warning: Reference `sec:measure-spaces' on page 18 undefined on input lin
e 61.

[18]

LaTeX Warning: Citation `Billingsley86' on page 19 undefined on input line 101.



LaTeX Warning: Reference `sec:sigma' on page 19 undefined on input line 105.

[19]

LaTeX Warning: Reference `sec:stepwise-approach' on page 20 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [20]
Chapter 4.

LaTeX Warning: Reference `sec:preliminaries' on page 21 undefined on input line
 10.


LaTeX Warning: Reference `sec:realrandvar' on page 21 undefined on input line 2
9.

[21])
No file root.bbl.
[22] (./root.aux)

Package rerunfilecheck Warning: File `root.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.


LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx9.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmm
i8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi9.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dis
t/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cms
y7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/t
exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (23 pages, 293214 bytes).
Transcript written on root.log.
This is BibTeX, Version 0.99d (TeX Live 2015/Debian)
The top-level auxiliary file: root.aux
The style file: plain.bst
Database file #1: root.bib
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./root.toc)pdfTeX warning (ext4): destinati
on with the same identifier (name{page.1}) has been already used, duplicate ign
ored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably

LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 16.


LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 38.

[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex

LaTeX Warning: Citation `hurd2002' on page 4 undefined on input line 30.

[4] [5]
Overfull \hbox (3.61127pt too wide) in paragraph at lines 401--414
[][]\OT1/cmr/bx/n/10 lemma as-sumes \OT1/cmr/m/it/10 s$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 sigma[]algebra a \OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 sigma[]alg
ebra[]UNIV$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 UNIV $\OMS/cmsy/m/n/10 2$ \OT1/c
mr/m/it/10 a$\OMS/cmsy/m/n/10 h[]i$[] 
) (./MonConv.tex

LaTeX Warning: Citation `Nipkow93' on page 6 undefined on input line 39.


LaTeX Warning: Citation `wenzelax' on page 6 undefined on input line 39.

[6]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 7 undefined on input line 9
7.

[7] [8]) (./Measure.tex

LaTeX Warning: Citation `hurd2002' on page 9 undefined on input line 28.

[9]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 10 undefined on input line 
79.


LaTeX Warning: Citation `Williams.mart' on page 10 undefined on input line 88.


LaTeX Warning: Citation `Bauer' on page 10 undefined on input line 107.

[10]

LaTeX Warning: Reference `nnfis' on page 11 undefined on input line 295.

) [11] (./RealRandVar.tex

LaTeX Warning: Citation `Skalberg' on page 12 undefined on input line 35.


LaTeX Warning: Citation `mesfunc1' on page 12 undefined on input line 47.


LaTeX Warning: Citation `mesfunc2' on page 12 undefined on input line 47.


LaTeX Warning: Citation `hurd2002' on page 12 undefined on input line 56.

[12]

LaTeX Warning: Citation `Billingsley86' on page 13 undefined on input line 86.


LaTeX Warning: Citation `Bauer' on page 13 undefined on input line 88.

[13]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 14 undefined on input line 
749.


Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[14] [15] [16]) [17]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 24.


LaTeX Warning: Citation `Bauer' on page 18 undefined on input line 25.


LaTeX Warning: Citation `Billingsley86' on page 18 undefined on input line 37.


LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 53.

[18]

LaTeX Warning: Citation `Billingsley86' on page 19 undefined on input line 101.


[19]

LaTeX Warning: Reference `sec:stepwise-approach' on page 20 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [20]
Chapter 4.
[21]) (./root.bbl [22]) [23] [24] (./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx9.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmm
i8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi9.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dis
t/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cms
y7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/t
exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (25 pages, 302499 bytes).
Transcript written on root.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty
Including comment 'isadelimproof' Excluding comment 'isatagproof'
Including comment 'isadelimML' Excluding comment 'isatagML') (./isabellesym.sty
) (./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./root.toc)pdfTeX warning (ext4): destinati
on with the same identifier (name{page.1}) has been already used, duplicate ign
ored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably
[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex [4] [5]
Overfull \hbox (3.61127pt too wide) in paragraph at lines 401--414
[][]\OT1/cmr/bx/n/10 lemma as-sumes \OT1/cmr/m/it/10 s$\OT1/cmr/m/n/10 :$ \OT1/
cmr/m/it/10 sigma[]algebra a \OT1/cmr/bx/n/10 shows \OT1/cmr/m/it/10 sigma[]alg
ebra[]UNIV$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 UNIV $\OMS/cmsy/m/n/10 2$ \OT1/c
mr/m/it/10 a$\OMS/cmsy/m/n/10 h[]i$[] 
) (./MonConv.tex [6] [7] [8]) (./Measure.tex [9] [10]

LaTeX Warning: Reference `nnfis' on page 11 undefined on input line 295.

) [11] (./RealRandVar.tex [12] [13]
Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[14] [15] [16]) [17]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 24.


LaTeX Warning: Reference `sec:stepwise-approach' on page 18 undefined on input 
line 53.

[18] [19]

LaTeX Warning: Reference `sec:stepwise-approach' on page 20 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [20]
Chapter 4.
[21]) (./root.bbl [22]) [23] [24] (./root.aux)

LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmm
i9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist
/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cms
y8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb>
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/
share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (25 pages, 296609 bytes).
Transcript written on root.log.

This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
No file root.aux.
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}]pdfTeX warning (ext4): destination with the s
ame identifier (name{page.1}) has been already used, duplicate ignored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably

LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 16.


LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 38.

[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex

LaTeX Warning: Reference `sec:measure-spaces' on page 4 undefined on input line
 29.


LaTeX Warning: Citation `hurd2002' on page 4 undefined on input line 30.

[4] [5] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [6] [7])
(./MonConv.tex

LaTeX Warning: Citation `Nipkow93' on page 8 undefined on input line 39.


LaTeX Warning: Citation `wenzelax' on page 8 undefined on input line 39.

[8]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 9 undefined on input line 9
7.

[9] [10] [11]) (./Measure.tex

LaTeX Warning: Citation `hurd2002' on page 12 undefined on input line 28.

[12]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 13 undefined on input line 
79.


LaTeX Warning: Citation `Williams.mart' on page 13 undefined on input line 88.


LaTeX Warning: Citation `Bauer' on page 13 undefined on input line 107.

[13] [14]

LaTeX Warning: Reference `nnfis' on page 15 undefined on input line 295.

[15] [16]) [17] (./RealRandVar.tex

LaTeX Warning: Citation `Skalberg' on page 18 undefined on input line 35.


LaTeX Warning: Reference `sec:measure-spaces' on page 18 undefined on input lin
e 42.


LaTeX Warning: Citation `mesfunc1' on page 18 undefined on input line 47.


LaTeX Warning: Citation `mesfunc2' on page 18 undefined on input line 47.


LaTeX Warning: Citation `hurd2002' on page 18 undefined on input line 56.

[18]

LaTeX Warning: Citation `Billingsley86' on page 19 undefined on input line 86.


LaTeX Warning: Citation `Bauer' on page 19 undefined on input line 88.

[19]

LaTeX Warning: Reference `sec:measure-spaces' on page 20 undefined on input lin
e 263.

[20] [21] [22] [23]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 24 undefined on input line 
749.


Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[24] [25]
Overfull \hbox (15.83801pt too wide) in paragraph at lines 1123--1125
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 rv[]plus[]rv rv[]square diff[]conv[]add[]uminus
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 add[]uminus[]conv[]diff$\OT1/cmr/m/n/1
0 )$[] 
[26] [27] [28]) [29]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 24.


LaTeX Warning: Citation `Bauer' on page 30 undefined on input line 25.


LaTeX Warning: Citation `Billingsley86' on page 30 undefined on input line 37.


LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 53.


LaTeX Warning: Reference `sec:measure-spaces' on page 30 undefined on input lin
e 61.

[30]

LaTeX Warning: Citation `Billingsley86' on page 31 undefined on input line 101.



LaTeX Warning: Reference `sec:sigma' on page 31 undefined on input line 105.

[31]

LaTeX Warning: Reference `sec:stepwise-approach' on page 32 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [32]
Chapter 4.

LaTeX Warning: Reference `sec:preliminaries' on page 33 undefined on input line
 10.


LaTeX Warning: Reference `sec:realrandvar' on page 33 undefined on input line 2
9.

[33])
No file root.bbl.
[34] (./root.aux)

Package rerunfilecheck Warning: File `root.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.


LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmbx9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi9.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
sy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf
-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (35 pages, 337020 bytes).
Transcript written on root.log.
This is BibTeX, Version 0.99d (TeX Live 2015/Debian)
The top-level auxiliary file: root.aux
The style file: plain.bst
Database file #1: root.bib
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./root.toc)pdfTeX warning (ext4): destinati
on with the same identifier (name{page.1}) has been already used, duplicate ign
ored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably

LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 16.


LaTeX Warning: Citation `hurd2002' on page 2 undefined on input line 38.

[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex

LaTeX Warning: Citation `hurd2002' on page 4 undefined on input line 30.

[4] [5] (/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [6] [7])
(./MonConv.tex

LaTeX Warning: Citation `Nipkow93' on page 8 undefined on input line 39.


LaTeX Warning: Citation `wenzelax' on page 8 undefined on input line 39.

[8]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 9 undefined on input line 9
7.

[9] [10] [11]) (./Measure.tex

LaTeX Warning: Citation `hurd2002' on page 12 undefined on input line 28.

[12]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 13 undefined on input line 
79.


LaTeX Warning: Citation `Williams.mart' on page 13 undefined on input line 88.


LaTeX Warning: Citation `Bauer' on page 13 undefined on input line 107.

[13] [14]

LaTeX Warning: Reference `nnfis' on page 15 undefined on input line 295.

[15] [16]) [17] (./RealRandVar.tex

LaTeX Warning: Citation `Skalberg' on page 18 undefined on input line 35.


LaTeX Warning: Citation `mesfunc1' on page 18 undefined on input line 47.


LaTeX Warning: Citation `mesfunc2' on page 18 undefined on input line 47.


LaTeX Warning: Citation `hurd2002' on page 18 undefined on input line 56.

[18]

LaTeX Warning: Citation `Billingsley86' on page 19 undefined on input line 86.


LaTeX Warning: Citation `Bauer' on page 19 undefined on input line 88.

[19] [20] [21] [22] [23]

LaTeX Warning: Citation `Fleuriot:2000:MNR' on page 24 undefined on input line 
749.


Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[24] [25]
Overfull \hbox (15.83801pt too wide) in paragraph at lines 1123--1125
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 rv[]plus[]rv rv[]square diff[]conv[]add[]uminus
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 add[]uminus[]conv[]diff$\OT1/cmr/m/n/1
0 )$[] 
[26] [27] [28]) [29]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 24.


LaTeX Warning: Citation `Bauer' on page 30 undefined on input line 25.


LaTeX Warning: Citation `Billingsley86' on page 30 undefined on input line 37.


LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 53.

[30]

LaTeX Warning: Citation `Billingsley86' on page 31 undefined on input line 101.


[31]

LaTeX Warning: Reference `sec:stepwise-approach' on page 32 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [32]
Chapter 4.
[33]) (./root.bbl [34]) [35] [36] (./root.aux)

LaTeX Warning: There were undefined references.


LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmbx9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi9.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
sy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf
-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (37 pages, 345398 bytes).
Transcript written on root.log.
This is pdfTeX, Version 3.14159265-2.6-1.40.16 (TeX Live 2015/Debian) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
LaTeX2e <2016/02/01>
Babel <3.9q> and hyphenation patterns for 81 language(s) loaded.

(./root.tex (/usr/share/texlive/texmf-dist/tex/latex/base/report.cls
Document Class: report 2014/09/29 v1.4h Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size11.clo))
(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.sty
(/usr/share/texlive/texmf-dist/tex/generic/babel-english/english.ldf
(/usr/share/texlive/texmf-dist/tex/generic/babel/babel.def)))
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/utf8.def
(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/ot1enc.dfu)
(/usr/share/texlive/texmf-dist/tex/latex/base/omsenc.dfu)))
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/stmaryrd.sty)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/wasysym.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/eufrak.sty

Package eufrak Warning: The eufrak package is redundant if the amsfonts package
 is used on input line 36.

) (/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def
(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.dfu))) (./isabelle.sty
(./comment.sty Excluding comment 'comment') Including comment 'isadelimtheory'
Including comment 'isatagtheory' Including comment 'isadelimproof'
Including comment 'isatagproof' Including comment 'isadelimML'
Including comment 'isatagML' Including comment 'isadelimvisible'
Including comment 'isatagvisible' Excluding comment 'isadeliminvisible'
Excluding comment 'isataginvisible') (./isabelletags.sty) (./isabellesym.sty)
(./pdfsetup.sty (/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/color.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty)
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty))))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty))

Package hyperref Message: Driver (autodetected): hpdftex.

(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty))
(./root.aux) (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd)
(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty))
(./root.out) (./root.out)
(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/stmaryrd/Ustmry.fd)
(/usr/share/texlive/texmf-dist/tex/latex/wasysym/uwasy.fd) [1{/var/lib/texmf/fo
nts/map/pdftex/updmap/pdftex.map}] (./root.toc)pdfTeX warning (ext4): destinati
on with the same identifier (name{page.1}) has been already used, duplicate ign
ored
<to be read again> 
                   \relax 
l.52 \newpage
              [1] (./intro.tex
Chapter 1.

Overfull \hbox (5.30475pt too wide) in paragraph at lines 6--13
[]\OT1/cmr/m/n/10.95 Verifying more ex-am-ples of prob-a-bilis-tic al-go-rithms
 will in-evitably
[2] [3]
Chapter 2.
) (./Sigma_Algebra.tex [4] [5]
(/usr/share/texlive/texmf-dist/tex/latex/base/omscmr.fd) [6] [7])
(./MonConv.tex [8] [9] [10] [11]) (./Measure.tex [12] [13] [14]

LaTeX Warning: Reference `nnfis' on page 15 undefined on input line 295.

[15] [16]) [17] (./RealRandVar.tex [18] [19] [20] [21] [22] [23]
Overfull \hbox (19.50415pt too wide) in paragraph at lines 746--753
[]\OT1/cmr/m/n/10.95 Of course, the ra-tio-nals come to mind. They were not ava
il-able in Isabelle/HOL[][][][][],
[24] [25]
Overfull \hbox (15.83801pt too wide) in paragraph at lines 1123--1125
[][]      \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp add$\OT1
/cmr/m/n/10 :$ \OT1/cmr/m/it/10 rv[]plus[]rv rv[]square diff[]conv[]add[]uminus
 del$\OT1/cmr/m/n/10 :$ \OT1/cmr/m/it/10 add[]uminus[]conv[]diff$\OT1/cmr/m/n/1
0 )$[] 
[26] [27] [28]) [29]
Chapter 3.

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 65.

(./Failure.tex

LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 24.


LaTeX Warning: Reference `sec:stepwise-approach' on page 30 undefined on input 
line 53.

[30] [31]

LaTeX Warning: Reference `sec:stepwise-approach' on page 32 undefined on input 
line 125.

) (./Integral.tex) (./outro.tex [32]
Chapter 4.
[33]) (./root.bbl [34]) [35] [36] (./root.aux)

LaTeX Warning: There were undefined references.

 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbsy10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/
amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
mmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi9.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/font
s/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/
public/amsfonts/cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/c
msy5.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy9.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texliv
e/texmf-dist/fonts/type1/public/amsfonts/cm/cmti9.pfb>
Output written on root.pdf (37 pages, 339838 bytes).
Transcript written on root.log.

*** Failed to apply initial proof method (line 1828 of "~~/afp/thys/Integration/Integral.thy"):
*** using this:
***   \<forall>y. \<exists>N. \<forall>n\<ge>N. y < 2 ^ n
*** goal (1 subgoal):
***  1. (\<lambda>n. inverse (2 ^ n)) \<longlonglongrightarrow> 0
*** At command "by" (line 1828 of "~~/afp/thys/Integration/Integral.thy")