[isabelle-dev] Broken session

[Jasmin Christian Blanchette]

Sorry, fixed (81ee85f56e2d).

Jasmin

Am 01.11.2013 um 21:06 schrieb Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev