infix 2 ==>
infix 3 OR ||
infix 4 AND &&
infix 5 == <>;
infix 3 OR
infix 4 AND;
infix 5 IMPLIES INTERSECTS;
nonfix --;

functor LOGIC() : LOGICSIG = 
    BDD(structure Lib     = LIBBDD()
	and Proposition   = Proposition				 
	structure Lit2Var = DICTIONARY(type Key = Proposition.Lit (* val < = Proposition.< *) )
	structure Var2Lit = DICTIONARY(type Key = Lib.Var)
				    );