Hi, complete_univ has been renamed to complete_UNIV in Isabelle 1a13325269c2 (after the fork for the release). I therefore assume that I can commit the relevant changes to afp-devel.
Best, Fabian Am 31.10.2013 um 10:53 schrieb Florian Haftmann <[email protected]>: >> Ordinary_Differential_Equations FAILED >> (see also >> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/Ordinary_Differential_Equations) >> >> sr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/share/texmf >> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb></usr/share/texmf-dist/fonts/ty >> pe1/public/amsfonts/cm/cmmi7.pfb></usr/share/texmf-dist/fonts/type1/public/amsf >> onts/cm/cmmi8.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.p >> fb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/ >> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb></usr/share/texmf-dist/font >> s/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texmf-dist/fonts/type1/public/a >> msfonts/cm/cmr8.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmssi >> 10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/s >> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texmf-dist >> /fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts/type1/pu >> blic/amsfonts/cm/cmti10.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/ >> symbols/msbm10.pfb> >> Output written on root.pdf (97 pages, 436697 bytes). >> Transcript written on root.log. >> >> *** Unknown fact "complete_univ" (line 449 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >> *** At command "using" (line 448 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Initial_Value_Problem.thy") >> *** Unknown fact "complete_univ" (line 384 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") >> *** At command "using" (line 384 of >> "/mnt/home/haftmann/data/afp/master/thys/Ordinary_Differential_Equations/Auxiliarities.thy") > > This refers to Isabelle 6d0688ce4ee2 and AFP 2a0f81020af9 > > Any ideas? > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
