Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6) (format=pdflatex 2009.3.10) 24 JAN 2011 13:10
entering extended mode
%&-line parsing enabled.
**\nonstopmode\input{root.tex}
(./root.tex (/usr/share/texmf/tex/latex/base/article.cls
Document Class: article 2005/09/16 v1.4f Standard LaTeX document class
(/usr/share/texmf/tex/latex/base/size11.clo
File: size11.clo 2005/09/16 v1.4f Standard LaTeX file (size option)
)
\c@part=\count79
\c@section=\count80
\c@subsection=\count81
\c@subsubsection=\count82
\c@paragraph=\count83
\c@subparagraph=\count84
\c@figure=\count85
\c@table=\count86
\abovecaptionskip=\skip41
\belowcaptionskip=\skip42
\bibindent=\dimen102
) (./isabelle.sty
\isa@parindent=\dimen103
\isa@parskip=\dimen104
(/usr/share/texmf/tex/latex/comment/comment.sty
\CommentStream=\write3
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')
(./isabellesym.sty) (/usr/share/texmf/tex/latex/amsmath/amsmath.sty
Package: amsmath 2000/07/18 v2.13 AMS math features
\@mathmargin=\skip43
For additional information on amsmath, use the `?' option.
(/usr/share/texmf/tex/latex/amsmath/amstext.sty
Package: amstext 2000/06/29 v2.01
(/usr/share/texmf/tex/latex/amsmath/amsgen.sty
File: amsgen.sty 1999/11/30 v2.0
\@emptytoks=\toks14
\ex@=\dimen105
))
(/usr/share/texmf/tex/latex/amsmath/amsbsy.sty
Package: amsbsy 1999/11/29 v1.2d
\pmbraise@=\dimen106
)
(/usr/share/texmf/tex/latex/amsmath/amsopn.sty
Package: amsopn 1999/12/14 v2.01 operator names
)
\inf@bad=\count87
LaTeX Info: Redefining \frac on input line 211.
\uproot@=\count88
\leftroot@=\count89
LaTeX Info: Redefining \overline on input line 307.
\classnum@=\count90
\DOTSCASE@=\count91
LaTeX Info: Redefining \ldots on input line 379.
LaTeX Info: Redefining \dots on input line 382.
LaTeX Info: Redefining \cdots on input line 467.
\Mathstrutbox@=\box26
\strutbox@=\box27
\big@size=\dimen107
LaTeX Font Info: Redeclaring font encoding OML on input line 567.
LaTeX Font Info: Redeclaring font encoding OMS on input line 568.
\macc@depth=\count92
\c@MaxMatrixCols=\count93
\dotsspace@=\muskip10
\c@parentequation=\count94
\dspbrk@lvl=\count95
\tag@help=\toks15
\row@=\count96
\column@=\count97
\maxfields@=\count98
\andhelp@=\toks16
\eqnshift@=\dimen108
\alignsep@=\dimen109
\tagshift@=\dimen110
\tagwidth@=\dimen111
\totwidth@=\dimen112
\lineht@=\dimen113
\@envbody=\toks17
\multlinegap=\skip44
\multlinetaggap=\skip45
\mathdisplay@stack=\toks18
LaTeX Info: Redefining \[ on input line 2666.
LaTeX Info: Redefining \] on input line 2667.
) (./pdfsetup.sty
(/usr/share/texmf/tex/latex/graphics/color.sty
Package: color 2005/11/14 v1.0j Standard LaTeX Color (DPC)
(/usr/share/texmf/tex/latex/config/color.cfg
File: color.cfg 2007/01/18 v1.5 color configuration of teTeX/TeXLive
)
Package color Info: Driver file: pdftex.def on input line 130.
(/usr/share/texmf/tex/latex/pdftex-def/pdftex.def
File: pdftex.def 2007/01/08 v0.04d Graphics/color for pdfTeX
\Gread@gobject=\count99
)))
(/usr/share/texmf/tex/latex/hyperref/hyperref.sty
Package: hyperref 2007/02/07 v6.75r Hypertext links for LaTeX
(/usr/share/texmf/tex/latex/graphics/keyval.sty
Package: keyval 1999/03/16 v1.13 key=value parser (DPC)
\KV@toks@=\toks19
)
\@linkdim=\dimen114
\Hy@linkcounter=\count100
\Hy@pagecounter=\count101
(/usr/share/texmf/tex/latex/hyperref/pd1enc.def
File: pd1enc.def 2007/02/07 v6.75r Hyperref: PDFDocEncoding definition (HO)
)
(/usr/share/texmf/tex/latex/config/hyperref.cfg
File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive
)
(/usr/share/texmf/tex/latex/oberdiek/kvoptions.sty
Package: kvoptions 2006/08/22 v2.4 Connects package keyval with LaTeX options (
HO)
)
Package hyperref Info: Option `colorlinks' set `true' on input line 2238.
Package hyperref Info: Hyper figures OFF on input line 2288.
Package hyperref Info: Link nesting OFF on input line 2293.
Package hyperref Info: Hyper index ON on input line 2296.
Package hyperref Info: Plain pages OFF on input line 2303.
Package hyperref Info: Backreferencing OFF on input line 2308.
Implicit mode ON; LaTeX internals redefined
Package hyperref Info: Bookmarks ON on input line 2444.
(/usr/share/texmf/tex/latex/ltxmisc/url.sty
\Urlmuskip=\muskip11
Package: url 2005/06/27 ver 3.2 Verb mode for urls, etc.
)
LaTeX Info: Redefining \url on input line 2599.
\Fld@menulength=\count102
\Field@Width=\dimen115
\Fld@charsize=\dimen116
\Choice@toks=\toks20
\Field@toks=\toks21
Package hyperref Info: Hyper figures OFF on input line 3102.
Package hyperref Info: Link nesting OFF on input line 3107.
Package hyperref Info: Hyper index ON on input line 3110.
Package hyperref Info: backreferencing OFF on input line 3117.
Package hyperref Info: Link coloring ON on input line 3120.
\Hy@abspage=\count103
\c@Item=\count104
\c@Hfootnote=\count105
)
*hyperref using default driver hpdftex*
(/usr/share/texmf/tex/latex/hyperref/hpdftex.def
File: hpdftex.def 2007/02/07 v6.75r Hyperref driver for pdfTeX
\Fld@listcount=\count106
)
No file root.aux.
\openout1 = `root.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 42.
LaTeX Font Info: ... okay on input line 42.
Package hyperref Info: Link coloring ON on input line 42.
(/usr/share/texmf/tex/latex/hyperref/nameref.sty
Package: nameref 2006/12/27 v2.28 Cross-referencing by name of section
(/usr/share/texmf/tex/latex/oberdiek/refcount.sty
Package: refcount 2006/02/20 v3.0 Data extraction from references (HO)
)
\c@section@level=\count107
)
LaTeX Info: Redefining \ref on input line 42.
LaTeX Info: Redefining \pageref on input line 42.
(./root.out) (./root.out)
\@outlinefile=\write4
\openout4 = `root.out'.
Package hyperref Warning: old toc file detected, not used; run LaTeX again.
\tf@toc=\write5
\openout5 = `root.toc'.
(./session.tex (./Myhill.tex [1
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}]
LaTeX Font Info: Try loading font information for OMS+cmr on input line 272.
(/usr/share/texmf/tex/latex/base/omscmr.fd
File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
)
LaTeX Font Info: Font shape `OMS/cmr/bx/n' in size <10> not available
(Font) Font shape `OMS/cmsy/b/n' tried instead on input line 272.
[2] [3] [4]
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@encoding' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<let>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@family' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@series' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@shape' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\font@name' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\OMX/cmex/m/n/7' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\ignorespaces' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `math shift' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\Rightarrow' on input line 533.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `math shift' on input line 533.
LaTeX Warning: Reference `example_eqns' on page 5 undefined on input line 539.
LaTeX Warning: Reference `example_eqns' on page 5 undefined on input line 553.
Overfull \hbox (32.24106pt too wide) in paragraph at lines 562--564
[]\OT1/cmr/m/n/10.95 In this for-mal-iza-tion, pure reg-u-lar ex-pres-sions lik
e $\OML/cmm/m/it/10.95 ^^U$ \OT1/cmr/m/n/10.95 is repsented by \OT1/cmr/m/it/10
.95 Lam$\OT1/cmr/m/n/10.95 ($\OT1/cmr/m/it/10.95 EMPTY$\OT1/cmr/m/n/10.95 )$,
[]
[5]
LaTeX Warning: Reference `example_eqns' on page 6 undefined on input line 628.
[6] [7] [8] [9] [10] [11] [12]
Overfull \hbox (25.68793pt too wide) in paragraph at lines 1396--1398
[][] \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 auto simp add$\
OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 ardenable[]def eqs[]def init[]rhs[]def rhs[]n
onempty[]def del$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 L[]rhs$\OML/cmm/m/it/10 :$\
OT1/cmr/m/it/10 simps$\OT1/cmr/m/n/10 )$[]
[]
[13]
Overfull \hbox (37.35094pt too wide) in paragraph at lines 1629--1642
[][]\OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 simp only$\OT1/cmr/
m/n/10 :$\OT1/cmr/m/it/10 rhs[]subst[]def append[]keeps[]nonempty nonempty[]se
t[]union nonempty[]set[]sub$\OT1/cmr/m/n/10 )$[]
[]
Overfull \hbox (6.14192pt too wide) in paragraph at lines 1669--1672
[][] \OT1/cmr/bx/n/10 have \OT1/cmr/m/it/10 rhs $\OT1/cmr/m/n/10 =$ $($\OT1/
cmr/m/it/10 rhs $\OMS/cmsy/m/n/10 ^^@$ \OT1/cmr/m/it/10 items[]of rhs X$\OT1/cm
r/m/n/10 )$ $\OMS/cmsy/m/n/10 [$ $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/10 items[]of
rhs X$\OT1/cmr/m/n/10 )$ \OT1/cmr/bx/n/10 by $\OT1/cmr/m/n/10 ($\OT1/cmr/m/it/1
0 auto simp$\OT1/cmr/m/n/10 :$\OT1/cmr/m/it/10 items[]of[]def$\OT1/cmr/m/n/10 )
$[]
[]
[14] [15] [16] [17] [18] [19] [20]
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@encoding' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<let>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@family' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@series' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@shape' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\font@name' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\OMX/cmex/m/n/7' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\ignorespaces' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `math shift' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\Rightarrow' on input line 2581.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `math shift' on input line 2581.
[21] [22] [23]
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@encoding' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<let>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@family' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@series' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@shape' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\font@name' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\OT1/cmr/m/it/12' on input line 3056.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\ignorespaces' on input line 3056.
[24] [25]
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@encoding' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<let>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@family' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@series' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@shape' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\font@name' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\OT1/cmr/m/it/12' on input line 3301.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\ignorespaces' on input line 3301.
[26]
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@encoding' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<let>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@family' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@series' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\f@shape' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\<def>-command' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\font@name' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\OT1/cmr/m/it/12' on input line 3375.
Package hyperref Warning: Token not allowed in a PDFDocEncoded string,
(hyperref) removing `\ignorespaces' on input line 3375.
[27] [28] [29])) [30] (./root.aux)
LaTeX Warning: There were undefined references.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
)
Here is how much of TeX's memory you used:
3589 strings out of 256216
46991 string characters out of 1917072
109661 words of memory out of 1500000
6815 multiletter control sequences out of 10000+200000
13669 words of font info for 48 fonts, out of 1200000 for 2000
645 hyphenation exceptions out of 8191
31i,8n,42p,736b,457s stack positions out of 5000i,500n,6000p,200000b,15000s
</usr/share/texmf/fonts/type1/bluesky/cm/cmbsy10.pfb></usr/share/texmf/fonts/
type1/bluesky/cm/cmbx10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmbx12.pfb
></usr/share/texmf/fonts/type1/bluesky/cm/cmex10.pfb></usr/share/texmf/fonts/ty
pe1/bluesky/cm/cmmi10.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmmi8.pfb></
usr/share/texmf/fonts/type1/bluesky/cm/cmr10.pfb></usr/share/texmf/fonts/type1/
bluesky/cm/cmr12.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmr17.pfb></usr/s
hare/texmf/fonts/type1/bluesky/cm/cmr7.pfb></usr/share/texmf/fonts/type1/bluesk
y/cm/cmr8.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmsy10.pfb></usr/share/t
exmf/fonts/type1/bluesky/cm/cmsy7.pfb></usr/share/texmf/fonts/type1/bluesky/cm/
cmsy8.pfb></usr/share/texmf/fonts/type1/bluesky/cm/cmti10.pfb></usr/share/texmf
/fonts/type1/bluesky/cm/cmti12.pfb>
Output written on root.pdf (30 pages, 175317 bytes).
PDF statistics:
257 PDF objects out of 1000 (max. 8388607)
44 named destinations out of 1000 (max. 131072)
105 words of extra memory for PDF output out of 10000 (max. 10000000)