diff -r e4d0e6cdc3d2 -r a1268fb0deea tphols-2011/generated/root.log --- a/tphols-2011/generated/root.log Wed Jan 26 22:58:24 2011 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,569 +0,0 @@ -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) -