Ignore:
Timestamp:
Dec 8, 2010, 6:08:05 PM (10 years ago)
Author:
campbell
Message:

A few more details in D3.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r392 r393  
    10511051nqed.
    10521052
    1053 ntheorem exec_inf_sound:
     1053ntheorem exec_inf_equivalence:
    10541054  ∀classic:(∀P:Prop.P ∨ ¬P).
    10551055  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
Note: See TracChangeset for help on using the changeset viewer.