Added refinement laws to deal with implicit operations and a basic specification refinement.