[isabelle-dev] Ordinary_Differential_Equations FAILED

[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 <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