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
2009-09-24 haftmann 2009-09-24 idempotency case for fold1
2009-09-24 haftmann 2009-09-24 added dual for complete lattice
2009-09-24 nipkow 2009-09-24 merged
2009-09-24 nipkow 2009-09-24 record how many "proof"s are solved by s/h
2009-09-24 boehmes 2009-09-24 added quotes for filenames; truncated remaining time (no floats supported by ulimit)
2009-09-24 bulwahn 2009-09-24 merged; adopted to changes from Code_Evaluation in the predicate compiler
2009-09-23 bulwahn 2009-09-23 replaced sorry by oops; removed old debug functions in predicate compiler
2009-09-23 bulwahn 2009-09-23 added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
2009-09-23 bulwahn 2009-09-23 adapted configuration for DatatypeCase.make_case