adjusted rep_datatype

Adapted to changes in perm_simp / swap_simps.

Replaced all but one occurrence of perm_simp_tac by perm_simproc_app, since perm_simp_tac now behaves in a different way (due to changes in swap_simps).

Rewrote code to use swap_simps rather than calc_atm (which tends to produce ridiculously large nested if-expressions).

moved HOL-Plain up;

rename Doc doc-src;

renamed Contents to Dirs to avoid case-conflict with doc/Contents;

section -> subsection

convert Isabelle CVS to Mercurial;

use begin and end for proofs in locales

exclude Distribution/bin/Isabelle;

init_theory: pass name explicitly; empty transition: empty name;

replaced datatype category constructivism by is_theory/is_proof;

Toplevel.init_theory: pass name explicitly;

command: always keep transition, not just as initial status; improved datatype category (moved here from outer_keyword.ML);

cached code for code antiquotation

code antiquotation roaring ahead

cleaned up some code generator configuration

tuned;

added datatype category;

replaced datatype kind by OuterKeyword.category;

clean: HOL-Plain;

prove lemma finite in context of finite class

added HOL-Plain;

explicit identification of toplevel commands, with status etc.; explicit point for tty mode; prompt: markup prev id; tuned signature;

added name_of; added get_id/put_id; tuned;

added get_id/put_id;

(removed Complex/ROOT.ML)

HOL += HOL-Complex

HOL += HOL-Complex