Added modules to po.hs
Added the skeleton for proof structuring constructs

o added a means for removing a universal quantifier in a goal
o added a test for when one does not remove universal quantifiers
o split the entailment proof obligation into two: assumption
containment and goal entailment
added proofs by case analysis
added some support for local assumptions
Added two proof elements:
o proof add assumption (can be used for a proof by contradiction)
o proof by "easy" (the command \easy doesn't print anything; can be
used to give a verbal argument)
Merge branch 'structured-proofs'
Added proofs by part. When a goal is formulated as a conjunction, one
can prove both conjuncts separately.
Added some flexibility in the expression parser to ignore spacing
commands
o changed the syntax to make assertions into commands instead of
environments. It allows us to free the LaTeX stylesheets from any
notion of align vs eqnarray
o improved the variable scopes in the parsing
o fixed the test cases to adopt the new syntax
o added some line info to error messages relating to mismatched \begin
/ \end
o changed assumes into commands
o added assert commands
o added line numbers to step proof obligations
o added command line options to the continuous program: -c makes it
continuous, -V makes it verbose, i.e. it prints the successful
verification conditions
added error messages for incorrect match of proofs and PO label
removed some commented code
Improved the pretty printing of the proof obligations
eliminated ~400 lines of commented dead code
o allowed referring to indiviual initialization clauses by label
o check that no assertion has generic parameters left in the types of
its subexpression
o added the \typeof{ expr }{ type } construct that allows the
disambiguation of the type of generic expression
enforced the type of assertions.
o improved the line number reporting on parsing expressions
o improved the ambiguity reports by reporting the smallest
subexpression for which the typing is unresolved
o improve the naming of generic parameter when reporting errors.
Merge branch 'structured-proofs'
split Document.Document into Document.Machine, Document.Proof and
Document.Visitor