NonEmptyArray is required to be nonempty
Allow arbitrary expression as length in CodeGeneration
Handle FiniteArray in valueToJVM
Add integration tests
finiteArray makes EmptyArray for arrays of size 0
Fail when z3 returns negative size array

Add some more helper functions/restructure
Handle LetDef in instantiateType

1) run's prototype follows apply's prototype: (ctx, v) instead of
(ctx)(v)

2) run() returns a possibly updated context. SimpleLeonPhase defines
apply and returns the same context.

(b) Adding support for inferring time, depth, stack and rec bounds
(c) Adding support for compositional reasoning in inferrence of time bounds
(d) Adding support for estimating stack usage at runtime
(e) Adding support for fractional literals

Fixes #143.

The test target `isabelle:test` now executes cleanly on Windows,
including bootstrapping.