[isabelle-dev] Broken session

[Florian Haftmann]

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

-------------- 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/20131101/742fbc20/attachment.asc>