[isabelle-dev] Build problems in AFP with current tips

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Jun 18 19:47:12 CEST 2014

isabelle: 88263522c31e tip
afp: b514f0bac50e tip

Completeness FAILED
*** Failed to load theory "Soundness" (unresolved "Completeness")
*** Extra variables on rhs: "founded", "bounded"
*** The error(s) above occurred in definition:
*** "proofTree A == bounded A & founded subs (SATAxiom o sequent) A"
*** At command "definition" (line 70 of
Random_Graph_Subgraph_Threshold FAILED
*** Failed to load theory "Ugraph_Lemmas" (unresolved "Prob_Lemmas")
*** Failed to load theory "Ugraph_Properties" (unresolved "Ugraph_Lemmas")
*** Failed to load theory "Subgraph_Threshold" (unresolved
*** Duplicate constant declaration "local.variance" vs. "local.variance"
(line 70 of
*** At command "definition" (line 70 of "/mnt/home/haftmann/data/afp
Markov_Models FAILED
*** Failed to apply initial proof method (line 488 of
*** using this:
***   integrable (paths s) f
***   0 <= f ?x
*** goal (1 subgoal):
***  1. integral\<^sup>L (paths s) f =
***     real (\<integral>\<^sup>+ x. ereal (f x) \<partial>paths s)
*** At command "by" (line 488 of



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140618/18e1cab3/attachment.asc>

More information about the isabelle-dev mailing list