Add example with nested quantifiers

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Fix bug in parse_arrow

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Allow notation to be associated with arbitrary expression (instead of only constants).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove verbosity.cpp, verbosity message channel should not be a global.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add interrupt method to type checker.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Remove interrupt.cpp. We changed the way we will handle interruptions in Lean.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Add interrupt to normalizer. Fix tests (they were not using the basic printer).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Use normalizer object in type checker. The idea is to make sure the interruption is propagated to normalizer.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Update .travis.yml and .travis.osx.yml
On Linux:
 - push to the repo on bitbucket, to trigger email-diff
 - push to the lean-osx repo on github, to trigger osx build & test
 - run test coverage and upload to dropbox
 - run doxygen and upload to dropbox
 - upload compiled binaries to dropbox

On OSX:
 - build & test
 - upload compiled binaries to dropbox
Implement dependencies on interval