The function Import.tDef now accepts a tactic (as well as a measure).

This allows L3 users to supply their own termination tactics.
Update Nat functions for parsing numbers from strings.

They should now return NONE in cases where they would previously raise an exception.
Minor tweaks to comments.