[isabelle-dev] AFP

[Tobias Nipkow]

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 
"/mnt/home/isatest/afp/devel/thys/RSAPSS/Wordarith.thy").

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)

Tobias