Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 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/extralib.ma

    r1930 r1949  
    4242qed.
    4343
    44 interpretation "logical iff" 'iff x y = (iff x y).
     44(* Paolo: already in library, generates ambiguity
     45interpretation "logical iff" 'iff x y = (iff x y).*)
    4546
    4647(* bool *)
Note: See TracChangeset for help on using the changeset viewer.