Fri, 24 Feb 2012 13:50:37 +0100 | huffman | avoid using Int.Pls_def in proofs | changeset | files |
Fri, 24 Feb 2012 13:37:23 +0100 | huffman | remove ill-formed lemmas word_pred_0_Min and word_m1_Min | changeset | files |
Fri, 24 Feb 2012 13:33:03 +0100 | huffman | remove ill-formed lemma of_bl_no; adapt proofs | changeset | files |
Fri, 24 Feb 2012 13:25:21 +0100 | huffman | adapt lemma mask_lem to respect int/bin distinction | changeset | files |
Fri, 24 Feb 2012 11:23:36 +0100 | blanchet | rephrase some slow "metis" calls | changeset | files |
Fri, 24 Feb 2012 11:23:35 +0100 | blanchet | added support for Alt-Ergo through Why3 (mostly for experimental purposes, e.g. polymorphism vs. monomorphization) | changeset | files |