array.ArraySorted is now generic, with type and order relation parameters

(that is, using number of occurrences)
No more definition of permutation using inductive predicates.
Impacts array.ArrayPermut; proof sessions updated.
Coq realizations for map.Occ and map.MapPermut;
proof session for array.ArrayPermut in progress

as follows:

maps:   permut_sub     -> permut
arrays: map_permut_sub -> permut     (to be consistent with maps)
        permut_sub     -> permut_sub
        permut         -> permut_all

- all programs with sessions are in examples/
- all programs without sessions are in examples/in_progress/
  (if you have private sessions for those, just move them there)
- all pure logical problems are in logic/
  (to simplify bench scripts and gallery building; they are few anyway)
- all OCaml programs are in examples/use_api/
- all strange stuff is in examples/misc/
  (most of it should probably go)
- Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
  (why do we need two sets of solutions for quite simple problems?)
- hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/

Bench scripts and documentation are updated.
Also, bench/bench is simplified a little bit.

new syntax 'L: to introduce a mark
new syntax at t 'L in logical expressions

- No more "and", "or", "implies", "iff", and "~".
  Use "/\", "\/", "->", "<->", and "not" instead.

- No more "logic". Use "function" or "predicate".

(Communications of the ACM)