licenses: convert license tags to SPDX
global: isabelle update_cartouches
lib: Improve documentation of Strengthen_Demo. Clarify that the second proof is essentially a forward reference to concepts that will be explained later in the file.
Demo theory for strengthen.