Changeset 2645 for src/ASM/BitVector.ma
- Timestamp:
- Feb 7, 2013, 9:22:22 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/BitVector.ma
r2601 r2645 10 10 include "ASM/FoldStuff.ma". 11 11 include "ASM/Vector.ma". 12 include "ASM/String.ma".13 12 14 13 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 226 225 qed. 227 226 228 (*229 axiom bitvector_of_string:230 ∀n: nat.231 ∀s: String.232 BitVector n.233 234 axiom string_of_bitvector:235 ∀n: nat.236 ∀b: BitVector n.237 String.238 *)239 240 227 lemma bitvector_3_cases: 241 228 ∀w: BitVector 3.
Note: See TracChangeset
for help on using the changeset viewer.