Better use of modules / less global polution for strings

See CHANGELOG for details

added 9 commits

• dca12791...d37b5e70 - 5 commits from branch master
• f290630d - Better use of modules for string, consistent with numbers.
• e1ee2d5f - We _can_ export notations.
• 46bc88e3 - Add order on strings.
• c88df915 - CHANGELOG.

Compare with previous version

added 1 commit

• 28d71c3c - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 8 commits

• 28d71c3c...2a3b41ca - 5 commits from branch master
• c8de231b - Better use of modules for string, consistent with numbers.
• 560412f0 - Add order on strings.
• 420bd785 - CHANGELOG.

Compare with previous version

resolved all threads

I think I addressed all your comments.

LGTM with the final changelog nit (we used the arrow in past changelogs and I think it makes this fairly easy to scan).

resolved all threads

added 1 commit

• 1dd6bcab - Tweak CHANGELOG.

Compare with previous version

enabled an automatic merge when the pipeline for 1dd6bcab succeeds

mentioned in commit bc76f1d5

merged

@iris-users This is a breaking change:

• Move all definitions and lemmas about strings/ascii into the modules String/Ascii, i.e., rename string_rev_app → String.rev_app, string_rev → String.rev, is_nat → Ascii.is_nat, is_space → Ascii.is_space and words → String.words.
• The file std.strings no longer exports the String module, it only exports the string type, its constructors, induction principles, and notations (in string_scope). Similar to the number types (nat, N, Z), importing the String module yourself is discouraged, rather use

The sed script will help you port your development.