[isabelle-dev] Coinductive FAILED

[Florian Haftmann]

isabelle b01057e72233 / afp 30c892926c46

> Coinductive FAILED
> (see also /mnt/home/haftmann/data/isabelle/devel/heaps/polyml-5.5.1_x86-linux/log/Coinductive)
> 
> s/type1/public/amsfonts/cm/cmsy5.pfb></usr/share/texmf-dist/fonts/type1/public/
> amsfonts/cm/cmsy7.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cms
> y8.pfb></usr/share/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/s
> hare/texmf-dist/fonts/type1/public/amsfonts/cm/cmti12.pfb></usr/share/texmf-dis
> t/fonts/type1/public/amsfonts/cm/cmtt10.pfb>
> Output written on root.pdf (303 pages, 845312 bytes).
> Transcript written on root.log.
> 
> *** Theory loader: failed to load "Coinductive_List_Prefix" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "Koenigslemma" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "Lazy_LList" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "Quotient_Coinductive_List" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "Coinductive_Stream" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "TLList" (unresolved "Coinductive_List")
> *** Theory loader: failed to load "Quotient_TLList" (unresolved "TLList")
> *** Theory loader: failed to load "Lazy_TLList" (unresolved "Lazy_LList", "TLList")
> *** Theory loader: failed to load "Coinductive" (unresolved "Coinductive_List_Prefix", "Coinductive_Stream", "Koenigslemma", "Quotient_Coinductive_List", "Quotient_TLList")
> *** Error in case expression:
> *** type mismatch
> *** At command "lemma" (line 873 of "/mnt/home/haftmann/data/afp/devel/thys/Coinductive/Coinductive_List.thy")

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de