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
2009-09-21 haftmann 2009-09-21 tuned proof; tuned headers
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proofs; be more cautios wrt. default simp rules
2009-09-21 haftmann 2009-09-21 merged
2009-09-21 haftmann 2009-09-21 tuned proofs
2009-09-19 haftmann 2009-09-19 merged
2009-09-19 haftmann 2009-09-19 inter and union are mere abbreviations for inf and sup
2009-09-24 haftmann 2009-09-24 merged
2009-09-24 haftmann 2009-09-24 lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
2009-09-24 haftmann 2009-09-24 subsumed by more general setup in List.thy