Changeset 1480


Ignore:
Timestamp:
Nov 2, 2011, 1:59:17 PM (8 years ago)
Author:
sacerdot
Message:

Proof changed (to use new automation).
BUG FOUND: automation fails if run in parallel on two goals belonging to
two different clusters. To be investigated.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Integers.ma

    r961 r1480  
    435435  ∀x,y. eq x y = eq y x.
    436436#x #y change with (eq_bv ??? = eq_bv ???)
    437  @eq_bv_elim @eq_bv_elim /2/
    438 #E >E * #NE @False_ind @NE @refl
     437 @eq_bv_elim @eq_bv_elim /2/ #H1 #H2 @⊥ [/2/ | /2/] (*Andrea: XXX*)
    439438qed.
    440439
Note: See TracChangeset for help on using the changeset viewer.