Implement Theorem-syntax form for save_thm

This switches to

Theorem foo[simp] = exp

to represent

val foo = save_thm("foo[simp]", exp)

Provide Theorem-syntax for save_thm (using quotation filter)

Testing it in ConseqConvScript.sml

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Remove trailing whitespace in source files.

Change src/bool to src/1 as a prelude to experimentation!