• Marianna Rapoport's avatar
    Making prophecy-related examples work with the new prophecy support · 1be9e3c6
    Marianna Rapoport authored
    - Removing admitted prophecy spec and making prophecy-related examples (coin-flip and atomic-pair-snapshot) work with the new prophecy support in heap_lang
    - Adjusting heap_lang tactics for automation of substitution, closedness, etc. to support prophecy syntax
    - Adding notation for prophecy syntax
    1be9e3c6
_CoqProject 3.68 KB