licenses: convert license tags to SPDX

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

Isabelle2018: new comment syntax

(result of "isabelle update_comments <dirs>")

lib: add theory LexordList, for lexicographical string comparison

By default, strings (and other lists) cannot be lexicographically
ordered because our theories pull in a conflicting instance of the
"order" class for lists. This theory adds a "lexord_list" wrapper type
that provides lexicographical order.