Ignore:
Timestamp:
Jul 17, 2012, 6:00:03 PM (8 years ago)
Author:
tranquil
Message:
  • updated joint semantics: generation of linear and graph semantics
  • opened two axioms in BitVectorZ
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2182 r2200  
    11include "joint/TranslateUtils_paolo.ma".
     2include "utilities/hide.ma".
    23
    34definition graph_to_lin_statement :
     
    1516#p#globals * [//] * //
    1617qed.
    17 
    18 definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
    19 definition hide_Prop : Prop → Prop ≝ λP.P.
    20 
    21 interpretation "hide proof" 'hide p = (hide_prf ? p).
    22 interpretation "hide Prop" 'hide p = (hide_Prop p).
    2318
    2419(* discard all elements passing test, return first element failing it *)
Note: See TracChangeset for help on using the changeset viewer.