strengthened and renamed lemma reflp_on_equality

renamed lemmas linorder.totalp_on_(ge|greater|le|less) and preorder.reflp_(ge|le)

Added an example for Isabelle/CTT

clarified signature;

clarified signature: more explicit types;

tuned output;

prefer sorted result;

separate style for re-use;

ML support for the Prism.js syntax highlighter -- via Isabelle/Scala;

retain data structures more accurately; tuned signature;

proper join without delimiter;

more accurate token types; keep untyped tokens for complete covering;

clarified JS namespace;

proper support for Windows;

support for the Prism.js syntax highlighter -- via external Node.js process;

support for JavaScript syntax and Node.js platform;

merged

tuned signature;

clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;

clarified signature: only support nameless separator;

tuned signature;

use timeout with MiniSat

merged

added lemma reflp_on_conversp[simp]

added lemma transp_reflclp[simp]

added lemma reflclp_ident_if_reflp[simp]

added lemma reflp_on_reflclp[simp]

strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp

more robust selection: avoid duplicates via "batch" number; evade attempts to select separator via keyboard or mouse (non-keyboard), assuming there are no consecutive separators;

tuned GUI;