A Datastructure for Iterated Powers

The current version of BshnFinal.v is 1.13 (April 16, 2006).

There is also a version BshnFinal81.v for use with Coq V8.1 pl2 (October 23, 2007).

Now also a version BshnFinal84.v tested with Coq V8.4 pl1 (December 28, 2012). It uses the library Vector instead of Bvector.

Ralph Matthes
Last modified: Fri Dec 28 11:07:26 CET 2012