Ignore:
Timestamp:
Mar 23, 2011, 4:39:01 PM (9 years ago)
Author:
sacerdot
Message:

Notations should NOT be redefined. Just add a new interpretation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/extralib.ma

    r697 r709  
    4242#A #x #y *;#H @nmk #H' /2/;
    4343qed.
    44 
    45 (* stolen from logic/connectives.ma to give Prop version. *)
    46 notation > "hvbox(a break \liff b)"
    47   left associative with precedence 25
    48 for @{ 'iff $a $b }.
    49 
    50 notation "hvbox(a break \leftrightarrow b)"
    51   left associative with precedence 25
    52 for @{ 'iff $a $b }.
    5344
    5445interpretation "logical iff" 'iff x y = (iff x y).
Note: See TracChangeset for help on using the changeset viewer.