[isabelle-dev] Ordinary_Differential_Equations FAILED

[Gerwin Klein]

Yes, you can commit freely to AFP-devel.

Cheers,
Gerwin

On 31 Oct 2013, at 9:33 pm, Fabian Immler <immler at in.tum.de> 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 <florian.haftmann at informatik.tu-muenchen.de>:
> 
>>> 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
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 273 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131031/5c1680f8/attachment.sig>