Changeset 874


Ignore:
Timestamp:
Jun 3, 2011, 10:13:35 AM (8 years ago)
Author:
sacerdot
Message:

Tactics no longer works.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r872 r874  
    333333  try %
    334334  [ 2: cases (sym_eq ??? prf); @tl
    335   | cases prf in tl H; #tl
     335  | generalize in match H; generalize in match tl; cases prf;
     336    (* cases prf in tl H; : ??? WAS WORKING BEFORE *)
     337    #tl
    336338    normalize in ⊢ (∀_: %. ?)
    337339    # H
Note: See TracChangeset for help on using the changeset viewer.