Yes, you can commit freely to AFP-devel. Cheers, Gerwin
On 31 Oct 2013, at 9:33 pm, Fabian Immler <[email protected]> wrote: > 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
