Changeset 2314 for src/ASM/Util.ma


Ignore:
Timestamp:
Aug 31, 2012, 4:12:35 PM (7 years ago)
Author:
campbell
Message:

Move generic definitions from recent commit to appropriate places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r2307 r2314  
    13891389qed.
    13901390
     1391lemma not_orb : ∀b,c:bool.
     1392  ¬ (b∨c) →
     1393  (bool_to_Prop (¬b))∧(bool_to_Prop (¬c)).
     1394* * normalize /2/
     1395qed.
     1396
    13911397lemma eq_false_to_notb: ∀b. b = false → ¬ b.
    13921398 *; /2 by eq_true_false, I/
Note: See TracChangeset for help on using the changeset viewer.