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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
