Update documentation about dispatch lists

[christiane-certora]

Update the grammar quite a bit (it was very outdated, still only had the deprecated syntax...), and add a section about dispatch list in the summaries.

Naming convention:

• PRs for features that are in design should have the "proposal" label
• PRs for features that haven't landed yet should have the "future" label
• PRs for upcoming releases should have the "release" label
• PRs with new documentation for existing features should have the "existing feature" label

Before requesting review:

• Make sure there is a ticket in the DOC board in Jira
• Make sure CI is passing
  • Spell check failure may require adding backticks around code or updating spelling_wordlist.txt
  • See README.md for information about style and markdown syntax
  • If the CI Details link gives a 404, you need to log in to readthedocs.com
• Add link to generated documentation here
  • you can find this by following the read the docs link from the CI check
• Ask for help in #documentation

Jira ticket: TODO
Link to generated documentation: https://certora-certora-prover-documentation--433.com.readthedocs.build/en/433/docs/cvl/methods.html

[johspaeth]

Thanks! looks good, just a few comments.

[johspaeth]

I am not sure I understand, what do you mean by this?

[christiane-certora]

That you shouldn't put "ALL" or "DELETE" or something like that at the end. I copied the wording from the catch-unresolved-calls section where it says "Also, the visibility is always external, and no policy should be specified."

[christiane-certora]

I'm adding "application" since we call it an application policy earlier.

[johspaeth]

Suggested change

	function _.foo() external => DISPATCH(true)[ C._, D._ ];
	function _.foo() external => DISPATCH(true)[ C.foo, D._ ];

...and then briefly explain that foo is implicit, so that we have both cases here.