Summary
- merged
- Makefile is no longer needed ("isabelle afp_build HLDE" generates binary "generated/hlde" as specified in Solve_Code.thy by Florian Haftmann
- tuned proofs
- updated op's
- adapted to reverted <= syntax
- merged
- updated op syntax
- dropped more lemmas that are now already part of Main
- merged
- reuse lemmas that are now in Main
- merged
- updated to backed out infixes in Set & Ordereings