hgrc for conversion and web service;

provide HGRCPATH, taken from cvs/Admin; replaced MERCURIAL by HG, which is also used by Mercurial internally;

code antiquotation roaring ahead

tuned

adjusted postprocessort setup

added lemma antiquotation

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;