Merge branch 'master' into refinement
Merge branch 'master' into refinement
todo list
remove dead code
o added refinement rules for progress properties
o declaration of progress properties
o proof obligation for safety properties
o added one proof strategy in the usual sequent proofs
o used more refinement rules in the examples.
o discharged one progress property
froze a test case
o inductive progress proofs
o added proofs by disjunction
o fixed the calculation of free variables in parsing progress properties
o added a proper test
o fixed for the proofs by disjunction
refactored the visitor to integrate it to the monad transformer
framework
Changed the visitor design to use monad transformers. Preparing for the
addition of a data structure to record the structure of progress proof
in order to check for cycles.
added a test (that still fails)
introduced the infrastructure for some visitors to have a customized
state.
Now detects cyclic refinements
Refactoring: changed the visitor design to remove the line info from
the parameter list of the individual visitors
Added a list of design principles
new todo, improved error message, better typesetting of variants in

inductive proofs.
Fixed line numbers in the parser.
o Added an implication rule.
o Added a function theorem to deal with (f | x0 → y).x1
o Added an example of phase synchronisation algorithm
o Made a variant of the cubes example where we keep producing cubes
without limits
o
removed a phony file
Merge branch 'refinement'