Fixed with 1bcf0828d38c and 7a2b867fa843. Am Montag, den 17.11.2014, 09:13 +0100 schrieb Florian Haftmann: > > isabelle: 059ba950a657 tip > > afp: 0fdf8f639bb4 tip > > Building HOL-Multivariate_Analysis ... > > Running Sturm_Tarski ... > > Running Abstract_Completeness ... > > Finished Sturm_Tarski (0:00:28 elapsed time, 0:01:21 cpu time, factor 2.89) > > > > Abstract_Completeness FAILED > > (see also > > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Abstract_Completeness) > > > > > > [20] [21] [22] [23] [24] [25]) (./Abstract_Completeness.tex) > > (./Propositional_Logic.tex [26] [27])) [28] (./root.aux) ) > > (see the transcript file for additional > > information)</usr/share/texmf-dist/font > > s/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texmf-dist/fonts/type1/public > > /amsfonts/cm/cmbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c > > mex10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us > > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-d > > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1 > > /public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/fonts/type1/public/amsfont > > s/cm/cmr7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb> > > </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/tex > > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb> > > Output written on root.pdf (28 pages, 198420 bytes). > > Transcript written on root.log. > > > > *** Failed to apply terminal proof method (line 128 of > > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy"): > > *** goal (1 subgoal): > > *** 1. ev (holds (op = r)) (rs @- flat (smap (%n. stake n rules) (fromN > > n))) > > *** At command "qed" (line 128 of > > "/mnt/home/haftmann/data/afp/master/thys/Abstract_Completeness/Abstract_Completeness.thy") > > Finished HOL-Multivariate_Analysis (0:03:18 elapsed time, 0:10:58 cpu time, > > factor 3.32) > > Building HOL-Probability ... > > Finished HOL-Probability (0:03:20 elapsed time, 0:11:32 cpu time, factor > > 3.46) > > Running Probabilistic_Noninterference ... > > > > Probabilistic_Noninterference FAILED > > (see also > > /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.2_x86-linux/log/Probabilistic_Noninterference) > > > > mr/m/n/10 )$ \OT1/cmr/bx/n/10 where \OT1/cmr/m/it/10 c1 $\OMS/cmsy/m/n/10 > > ^^Y$\ > > OT1/cmr/m/it/10 01 c2 $\OMS/cmsy/m/n/10 ^^Q$ $\OT1/cmr/m/n/10 > > ($\OT1/cmr/m/it/1 > > 0 c1$\OML/cmm/m/it/10 ;$\OT1/cmr/m/it/10 c2$\OT1/cmr/m/n/10 )$ > > $\OMS/cmsy/m/n/1 > > 0 2$ \OT1/cmr/m/it/10 Example[]PL$\OML/cmm/m/it/10 :$\OT1/cmr/m/it/10 > > ZObis[] > > [69])) (./root.bbl) [70] (./root.aux) ) > > (see the transcript file for additional > > information)</usr/share/texmf-dist/font > > s/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texmf-dist/fonts/type1/public > > /amsfonts/cm/cmbx12.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/c > > mex10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></us > > r/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texmf-d > > ist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texmf-dist/fonts/type1 > > /public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/fonts/type1/public/amsfont > > s/cm/cmr6.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb> > > </usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/tex > > mf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb> > > Output written on root.pdf (70 pages, 254440 bytes). > > Transcript written on root.log. > > > > *** Undefined constant: "T.hitting_time" (line 235 of > > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy") > > *** At command "abbreviation" (line 235 of > > "/mnt/home/haftmann/data/afp/master/thys/Probabilistic_Noninterference/Trace_Based.thy") > > Unfinished session(s): Abstract_Completeness, Probabilistic_Noninterference > > 0:08:36 elapsed time, 0:33:24 cpu time, factor 3.88 > > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
