Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (9 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r1882 r1949  
    134134] qed.
    135135
     136alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
    136137unification hint 0 ≔ X ;
    137138N ≟ max_def List
Note: See TracChangeset for help on using the changeset viewer.