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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
