licenses: convert license tags to SPDX

global: isabelle update_cartouches

lib: add non-cond-simplification, use in wpsimp.

Adds "non-conditional simplification" method simp_no_cond, and
various equivalents.

This is done by setting the simplifier depth limit to 0, which seems
to be a useful case. It prevents expensive conditional simplification
attempts but leaves the simplifier strategy otherwise unchanged.

This is easy to set up, and link to wpsimp.