[isabelle-dev] AFP

Tobias Nipkow nipkow at in.tum.de
Tue Jul 17 12:01:49 CEST 2007

The RSAPSS entry in the AFP no longer compiles. Here is the tail of the log:

lemma remzero_replicate: remzero (replicate ?n \<zero> @ ?l) = remzero ?l
lemma length_bvxor_bound: ?a <= length ?l ==> ?a <= length (bvxor ?l ?l2.0)
*** Ill-typed instantiation:
***   n :: nat
*** At command "proof" (line 110 of 

Some developer must have forgotten(!) to test the AFP when submitting a 
change. Can you please check if this is you? (And let me know)


More information about the isabelle-dev mailing list