diff -r c64241fa4dff -r f5db9e08effc tphols-2011/generated/root.log --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tphols-2011/generated/root.log Mon Jan 24 11:29:55 2011 +0000 @@ -0,0 +1,569 @@ +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 `\-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 `\-command' on input line 533. + + +Package hyperref Warning: Token not allowed in a PDFDocEncoded string, +(hyperref) removing `\-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 `\-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 `\-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 `\-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 `\-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 `\-command' on input line 2581. + + +Package hyperref Warning: Token not allowed in a PDFDocEncoded string, +(hyperref) removing `\-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 `\-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 `\-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 `\-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 `\-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 `\-command' on input line 3056. + + +Package hyperref Warning: Token not allowed in a PDFDocEncoded string, +(hyperref) removing `\-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 `\-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 `\-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 `\-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 `\-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 `\-command' on input line 3301. + + +Package hyperref Warning: Token not allowed in a PDFDocEncoded string, +(hyperref) removing `\-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 `\-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 `\-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 `\-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 `\-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 `\-command' on input line 3375. + + +Package hyperref Warning: Token not allowed in a PDFDocEncoded string, +(hyperref) removing `\-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 `\-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 `\-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 `\-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 + +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) +