Changeset 709 for src/utilities
 Timestamp:
 Mar 23, 2011, 4:39:01 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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