move proof of con_rews into domain_constructor.ML

don't bother returning con_defs

move constructor-specific stuff to a separate function

replace prove_thm function

move proof of compactness rules into domain_constructors.ML

add some convenience functions

rewrite domain package code for selector functions

add function beta_of_def

reorganizing domain package code (in progress)

change domain package's treatment of variable names in theorems to be like datatype package

remove redundant lemma real_minus_half_eq

polished and converted some proofs to Isar style

killed more recdefs

tuned comment

repaired subscripts broken in d8d7d1b785af

repaired definition (cf. d8d7d1b785af)

authentic syntax for *all* logical entities;

mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;

notation for xsymbols (cf. ad039d29e01c);

"_type_prop" is syntax const -- recovered printing of OFCLASS;

removed unused external_names;

cleanup type translations;

adapted to authentic syntax -- actual types are verbatim;

authentic syntax for classes and type constructors; read/intern formal entities just after raw parsing, extern just before final pretty printing; discontinued _class token translation; moved Local_Syntax.extern_term to Syntax/printer.ML; misc tuning;

more systematic mark/unmark operations; tuned;

proper (type_)notation;

proper antiquotations;

standard convention for syntax consts;

more precise scope of exception handler;

eliminated hard tabs;