/* style sheet for displaying insertions and deletions to a web page */
.ins { color: red; text-decoration: underline; }
.del { color: gray; text-decoration: line-through;}