Hi Florian, My bad again. Fixed (578371ba74cc). Now I see why "pervasive = true" makes sense.
Thanks for the notice. BTW is there any particular reason why testboard and tests are kind of dead these days? Jasmin Am 06.11.2013 um 21:12 schrieb Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>: > 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 > _______________________________________________ > 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
