2009-09-11 Thomas Sewell 2009-09-11 Implement previous fix (don't duplicate ext_def) correctly.
2009-09-11 Thomas Sewell 2009-09-11 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.
2009-09-11 Thomas Sewell 2009-09-11 Merged with mainline changes.
2009-09-11 Thomas Sewell 2009-09-11 Adjust some documentation.
2009-09-10 Thomas Sewell 2009-09-10 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.
2009-09-10 Thomas Sewell 2009-09-10 Record patch imported and working.
2009-08-27 tsewell 2009-08-27 Initial attempt at porting record update to repository Isabelle.
2009-09-29 wenzelm 2009-09-29 Synchronized and Unsynchronized;
2009-09-29 wenzelm 2009-09-29 hide "ref" by default, to enforce excplicit indication as Unsynchronized;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-29 wenzelm 2009-09-29 open_unsynchronized for interactive Isar loop;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-29 wenzelm 2009-09-29 Raw ML references as unsynchronized state variables.
2009-09-28 wenzelm 2009-09-28 Dummy version of state variables -- plain refs for sequential access.
2009-09-28 wenzelm 2009-09-28 reactivated at-sml-dev-e;
2009-09-28 wenzelm 2009-09-28 misc tuning and modernization;
2009-09-28 wenzelm 2009-09-28 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-28 wenzelm 2009-09-28 merged
2009-09-28 haftmann 2009-09-28 less auxiliary functions
2009-09-28 haftmann 2009-09-28 tuned
2009-09-28 haftmann 2009-09-28 shared code between rep_datatype and datatype
2009-09-28 haftmann 2009-09-28 further unification of datatype and rep_datatype
2009-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-28 wenzelm 2009-09-28 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;
2009-09-28 wenzelm 2009-09-28 tuned internal source structure;
2009-09-28 wenzelm 2009-09-28 added fork_deps_pri;
2009-09-28 haftmann 2009-09-28 merged
2009-09-28 haftmann 2009-09-28 explicit pointless checkpoint
2009-09-27 haftmann 2009-09-27 emerging common infrastructure for datatype and rep_datatype
2009-09-27 haftmann 2009-09-27 streamlined rep_datatype further
2009-09-27 haftmann 2009-09-27 simplified rep_datatype
2009-09-27 haftmann 2009-09-27 more appropriate order of field in dt_info
2009-09-27 haftmann 2009-09-27 re-established reasonable inner outline for module
2009-09-27 wenzelm 2009-09-27 merged
2009-09-27 haftmann 2009-09-27 adjusted to changes in datatype package
2009-09-27 haftmann 2009-09-27 merged
2009-09-27 haftmann 2009-09-27 dropped dead code
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-09-27 wenzelm 2009-09-27 fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
2009-09-27 wenzelm 2009-09-27 tuned;
2009-09-27 wenzelm 2009-09-27 reachable: recovered reverse post-order (lost in 73ad4884441f), which is expected for all_preds/all_succs and required for topological_order;
2009-09-25 paulson 2009-09-25 merged
2009-09-25 paulson 2009-09-25 New lemmas involving the real numbers, especially limits and series
2009-09-25 haftmann 2009-09-25 NEWS; corrected spelling
2009-09-25 haftmann 2009-09-25 merged
2009-09-23 haftmann 2009-09-23 simplified proof
2009-09-23 haftmann 2009-09-23 removed potentially dangerous rules from pred_set_conv
2009-09-23 haftmann 2009-09-23 explicitly hide empty, inter, union
2009-09-23 haftmann 2009-09-23 merged
2009-09-23 haftmann 2009-09-23 merged
2009-09-23 haftmann 2009-09-23 merged
2009-09-23 haftmann 2009-09-23 inf/sup_absorb are no default simp rules any longer
2009-09-22 haftmann 2009-09-22 merged
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 adapted proof
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-09-21 haftmann 2009-09-21 tuned header
2009-09-21 haftmann 2009-09-21 added note on simp rules
2009-09-21 haftmann 2009-09-21 merged