Started on adding counters to the big-step semantics
Fixing up proofs
More work on clocked big step semantics

The existing metatheory should all build again, and I've related the
clocked and unclocked big step semantics together.  I'm halfway through
proving totality for the clocked big step relation.
Oops, an oversight that broke determinism.
Finished the theorems about the clocked big step semantics
Merge branch 'master' into clock

To get the modules-ready compiler, to work on making it also build with
the clocked source semantics.
Get semanticsExtraTheory building with clocked source semantics

Skip all the enveq stuff since it's now (I think) not used in
compilerProofsTheory.
get pmatchTheory building with clocked source semantics
add Ctimeout_error to the intLang

(not using it in Cevaluate yet though)
remove evaluateEquationsTheory

because clearly nobody else was using it. copy things I probably am
using (automatic rewrites) into semanticsExtraTheory, and update for the
clock.
work on updating toIntLangProofsTheory for clocked source semantics
finish updating toIntLangProofsTheory
update compilerProofsTheory for clocked source semantics
Merge branch 'clock'

Compiler proofs now build with the clocked source semantics. However,
have not added a clock to the intermediate or bytecode semantics yet.