Allow theorems to be stored "locally", with local attributes

Such theorems are not stored in the exported theory, but do
temporarily affect the global contexts that their attributes point at.

The test-case illustrates this, with a local simp not visible in the
later theory.

Move theorem-attribute "parser" implementation to ThmAttribute.sml

Refactor handling of thm attributes ("simp", etc) into new module

A slight backwards incompatibility is that this removes the ability
for script files to declare new attributes (hence removal of
attr[12]Script.sml from src/1/theory_tests). This facility is used
vacuously in CakeML once.