Re: [isabelle-dev] Ordinary_Differential_Equations FAILED

2013-10-31 Thread Gerwin Klein 
Yes, you can commit freely to AFP-devel.

Cheers,
Gerwin

On 31 Oct 2013, at 9:33 pm, Fabian Immler  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 
> :
> 
>>> 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>>> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb>>> pe1/public/amsfonts/cm/cmmi7.pfb>>> onts/cm/cmmi8.pfb>>> fb>>> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb>>> s/type1/public/amsfonts/cm/cmr7.pfb>>> msfonts/cm/cmr8.pfb>>> 10.pfb>>> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb>>> /fonts/type1/public/amsfonts/cm/cmsy7.pfb>>> blic/amsfonts/cm/cmti10.pfb>>> 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-...@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



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Ordinary_Differential_Equations FAILED

2013-10-31 Thread Fabian Immler 
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 
:

>> 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>> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb>> pe1/public/amsfonts/cm/cmmi7.pfb>> onts/cm/cmmi8.pfb>> fb>> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb>> s/type1/public/amsfonts/cm/cmr7.pfb>> msfonts/cm/cmr8.pfb>> 10.pfb>> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb>> /fonts/type1/public/amsfonts/cm/cmsy7.pfb>> blic/amsfonts/cm/cmti10.pfb>> 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-...@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

[isabelle-dev] Ordinary_Differential_Equations FAILED

2013-10-31 Thread Florian Haftmann 
> 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> -dist/fonts/type1/public/amsfonts/cm/cmmi12.pfb> pe1/public/amsfonts/cm/cmmi7.pfb> onts/cm/cmmi8.pfb> fb> texmf-dist/fonts/type1/public/amsfonts/cm/cmr17.pfb> s/type1/public/amsfonts/cm/cmr7.pfb> msfonts/cm/cmr8.pfb> 10.pfb> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb> /fonts/type1/public/amsfonts/cm/cmsy7.pfb> blic/amsfonts/cm/cmti10.pfb> 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



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev