• Clément Fumex's avatar
    Coq realization of bv theory: · 1a0d9e4a
    Clément Fumex authored
    - generation in the makefile
    - proofs done
    Remove complex axioms from Pow2int in bv.why.
    Add guards in rotates axioms in bv.why.
    1a0d9e4a
Makefile.in 61.4 KB