There's no particular reason to duplicate the extension constant's definition under the name "ext_def", and it also prevents you having a field called ext.

Merged with mainline changes.

Adjust some documentation.

Simplification of various aspects of the IsTuple component of the new record package. Extensive documentation added in IsTuple.thy - it should now be possible to figure out what's going on from the sources supplied.

Record patch imported and working.

Initial attempt at porting record update to repository Isabelle.

Synchronized and Unsynchronized;

hide "ref" by default, to enforce excplicit indication as Unsynchronized;

explicit indication of Unsynchronized.ref;

open_unsynchronized for interactive Isar loop;

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