isabelle update_cartouches -c -t;

eliminated old defs;

prefer local fixes;

modernized header uniformly as section;

downshift of theory Parity in the hierarchy

leftover from 3ccafeb9a1d1

eliminiated clone

tuned headers;

modernized specifications;

removed obsolete ML files;

converted to Isar theory format;

Added > and >= sugar

* sane numerals (stage 2): plain "num" syntax (removed "#");

sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;

changed 2 to #2

added IMPP to HOL