use a new library XLib, only necessary ones are added
added the materials from SF: var/state/aexp/bexp/cmd/HoareLogic