Changeset 2830 for src


Ignore:
Timestamp:
Mar 8, 2013, 11:37:59 PM (7 years ago)
Author:
sacerdot
Message:

Added abstractions in front of cases daemon for code extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r2783 r2830  
    7777*)  (* pop_frame          ≝ *) ((λ_.λ_.λ_.λ_.λst.pop_ra … st))
    7878(*  (* post_op2           ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)*).
    79 cases daemon
     79[ #x cases daemon
     80| #globals #genv whd in ⊢ (% → ?); cases daemon ]
    8081qed.
Note: See TracChangeset for help on using the changeset viewer.