Changeset 889 for src/common
- Timestamp:
- Jun 6, 2011, 11:07:24 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Integers.ma
r747 r889 434 434 theorem eq_sym: 435 435 ∀x,y. eq x y = eq y x. 436 #x #y @eq_bv_elim @eq_bv_elim /2/ 436 #x #y change with (eq_bv ??? = eq_bv ???) 437 @eq_bv_elim @eq_bv_elim /2/ 437 438 [ #NE #E @False_ind >E in NE * /2/ 438 439 | #E #NE @False_ind >E in NE * /2/ … … 440 441 441 442 theorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y). 442 #x #y @eq_bv_elim #H @H qed.443 #x #y change with (if eq_bv ? x y then ? else ?) @eq_bv_elim #H @H qed. 443 444 444 445 theorem eq_true: ∀x. eq x x = true.
Note: See TracChangeset
for help on using the changeset viewer.