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

[Florian Haftmann]

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
"/mnt/home/haftmann/data/afp/master/thys/Completeness/Completeness.thy")
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
"Ugraph_Properties")
*** Duplicate constant declaration "local.variance" vs. "local.variance"
(line 70 of
"/mnt/home/haftmann/data/afp/master/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy")
*** At command "definition" (line 70 of "/mnt/home/haftmann/data/afp
Markov_Models FAILED
*** Failed to apply initial proof method (line 488 of
"/mnt/home/haftmann/data/afp/master/thys/Markov_Models/Discrete_Markov_Kernel.thy"):
*** 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
"/mnt/home/haftmann/data/afp/master/thys/Markov_Models/Discrete_Markov_Kernel.thy")

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>