Move "classic" Prosa to rt.classic namespace and update documentation

As a first step towards completing #53 (closed) and #54 (closed), this MR moves the "old" Prosa to the rt.classic namespace and updates the documentation to reflect the "modern" Prosa.

changed milestone to %Prosa v0.4

changed title from WIP: Move to "classic" Prosa to rt.classic namespace and update documentation to WIP: Move "classic" Prosa to rt.classic namespace and update documentation

mentioned in merge request !61 (merged)

Looks good to me. I have one question. You added README.md for restructuring/behavior and restructuring/model but not for restructuring/analysis, why?

analaysis/ still needs to be reorganized anyway. I‘ll do that as after aRTA has gone in; to avoid merge conflicts.

added 13 commits

• 1c0e8129 - proofloc.py: fix single-line proof pattern
• 51a0ef1a - proofloc.py: do not count proofs that have been commented out
• 339363fa - create_makefile.sh: support --without-classic
• 3da386de - Don't re-generate _CoqProject in create_makefile.sh
• 34931f6e - do not rely on vlib x <= y <= z auto-splitting
• eb2d5f1d - do not rely on vlib 'des' tactic
• 95b3c310 - do not use vlib 'edone' when plain 'eassumption' will do
• f725d71e - do not rely on simpl_sum_const tactic
• 17f392e3 - move unused helper lemmas/notations/tactics to rt.classic
• 0e69b03f - mention classic/util in README
• 928c81b8 - create_makefile.sh: add --only-classic option
• cc7146ab - cleanup create_makefile.sh
• eeff0a60 - document the --only-classic option

Compare with previous version

unmarked as a Work In Progress

As there have not been any comments to the contrary, I'll merge this now.

added 22 commits

• 3c2bd740 - 1 commit from branch master
• 238b35e5 - move classic Prosa into rt.classic namespace
• a1cbf4f9 - update Require'd module names to rt.classic namespace
• 24f877db - update paths in the known long proofs database
• 3ea12adc - Update top-level and classic/ READMEs
• dbbad1f8 - update documentation and guidelines
• 48cd7a54 - document additional guidelines
• fcf52c78 - update explanation of new Prosa's structure
• 4e3a737c - add READMEs to behavior and model modules
• 8ae21891 - proofloc.py: fix single-line proof pattern
• 4918b196 - proofloc.py: do not count proofs that have been commented out
• 525c94c8 - create_makefile.sh: support --without-classic
• bc20368f - Don't re-generate _CoqProject in create_makefile.sh
• 6eab134c - do not rely on vlib x <= y <= z auto-splitting
• 2630d3b1 - do not rely on vlib 'des' tactic
• f7550c93 - do not use vlib 'edone' when plain 'eassumption' will do
• f3d1c76f - do not rely on simpl_sum_const tactic
• a37f107c - move unused helper lemmas/notations/tactics to rt.classic
• 1dad4615 - mention classic/util in README
• 3b18aa36 - create_makefile.sh: add --only-classic option
• 8037703d - cleanup create_makefile.sh
• f4330fe0 - document the --only-classic option

Compare with previous version

enabled an automatic merge when the pipeline for f4330fe0 succeeds

merged