# [isabelle] Proof failed in HOL? (build with -o browser_info fails)

Hi proof authors,

`I wanted to generate HTML files for HOL and HOL-BNF, and both fails with
``this message:
`
HOL FAILED

` (see also
``/home/yannick/.isabelle/Isabelle2013-2/heaps/polyml-5.5.1_x86-linux/log/HOL)
`
### (!!x. ?f x = ?g x) ==> ?f = ?g
### Rule already declared as introduction (intro)
### (!!x y. ?A x y ==> ?B (?f x) (?g y)) ==> (?A ===> ?B) ?f ?g
### Ignoring conversion rule for operator Orderings.bot_class.bot
val it = fn: theory -> theory
val it = "Num.neg_numeral_class.neg_numeral": string
### Ignoring duplicate rewrite rule:
### nat (numeral ?k1) == numeral ?k1
PROOF FAILED for depth 2
PROOF FAILED for depth 2
PROOF FAILED for depth 3
PROOF FAILED for depth 3
PROOF FAILED for depth 3
PROOF FAILED for depth 3
PROOF FAILED for depth 4

` ### /home/yannick/apps/isabelle/lib/Tools/browser: ligne 96: epstopdf
``: commande introuvable
` ### Failed to produce pdf output
*** Failed to prepare dependency graph
HOL-Cardinals-Base CANCELLED
HOL-Cardinals CANCELLED
HOL-BNF CANCELLED
Unfinished session(s): HOL, HOL-BNF, HOL-Cardinals, HOL-Cardinals-Base
Why does it says “PROOF FAILED”? I have not altered any theory files.
If ever that matter, here is the exact command I used:
isabelle build -o browser_info -o document=pdf -v -c HOL-BNF
Doing the same for FOL is OK.
--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*