[isabelle-dev] Ordinary_Differential_Equations FAILED

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Oct 31 10:53:55 CET 2013


> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131031/79be7206/attachment.asc>


More information about the isabelle-dev mailing list