explicit indication of Unsynchronized.ref;

Raw ML references as unsynchronized state variables.

Dummy version of state variables -- plain refs for sequential access.

reactivated at-sml-dev-e;

misc tuning and modernization;

moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);

merged

less auxiliary functions

tuned

shared code between rep_datatype and datatype

further unification of datatype and rep_datatype

avoid compound fields in datatype info record

fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point;

tuned internal source structure;

added fork_deps_pri;

merged

explicit pointless checkpoint

emerging common infrastructure for datatype and rep_datatype

streamlined rep_datatype further

simplified rep_datatype

more appropriate order of field in dt_info

re-established reasonable inner outline for module

merged

adjusted to changes in datatype package

merged

dropped dead code

registering split rules and projected induction rules; ML identifiers more close to Isar theorem names

fold_body_thms/join_bodies: explicitly check for cyclic theorem references;