Merge with changes from isabelle dev repository.

Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up.

Branch merge for isabelle mainline updates.

Branch merge with updates from mainline isabelle.

Implement previous fix (don't duplicate ext_def) correctly.

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