Sorry, fixed (81ee85f56e2d). Jasmin
Am 01.11.2013 um 21:06 schrieb Florian Haftmann <[email protected]>: > This refers to Isabelle hg id b1d955791529 > >> Running HOL-Proofs-Extraction ... >> >> HOL-Predicate_Compile_Examples FAILED >> (see also >> /mnt/home/haftmann/data/isabelle/master/heaps/polyml-5.5.1_x86-linux/log/HOL-Predicate_Compile_Examples) >> >> Proving the elimination rules ... >> Proving the induction rule ... >> Proving the simplification rules ... >> Proofs for inductive predicate(s) "steps" >> Proving monotonicity ... >> Proving the introduction rules ... >> Proving the elimination rules ... >> Proving the induction rule ... >> Proving the simplification rules ... >> "{}" >> :: "(nat * proc) set" >> "{[0, Suc (Suc 0)], [Suc 0, Suc (Suc 0)], [Suc (Suc 0), 0], >> [Suc (Suc 0), Suc 0]}" >> :: "nat list set" >> "{[0, Suc (Suc 0)], [Suc 0, Suc (Suc 0)], [Suc (Suc 0), 0]} Un ..." >> :: "nat list set" >> *** exception UnequalLengths raised (line 566 of "library.ML") >> *** At command "code_pred" (line 841 of >> "~~/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy") >> *** exception UnequalLengths raised (line 566 of "library.ML") >> *** At command "code_pred" (line 17 of >> "~~/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy") > > Florian > > -- > > PGP available: > http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
