Changeset 2819


Ignore:
Timestamp:
Mar 8, 2013, 12:14:56 AM (6 years ago)
Author:
sacerdot
Message:

Proof obligation closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2818 r2819  
    463463   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    464464   〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
    465 cases daemon
     465%
    466466qed.
Note: See TracChangeset for help on using the changeset viewer.