licenses: convert license tags to SPDX

global: isabelle update_cartouches

Add some comments.

After discussion with others, it's clear this is not self-documenting.
A few comments might make it easier to understand what's going on.

Thanks to Matt Brecknell for the more explanatory example.

Attribute for adjusting preconds.

Should work for corres-like rules. Works on an example. Needs
real testing.