src/ZF/Order.ML
1999-09-21 nipkow 1999-09-21 Mod because of new solver interface.
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-02-03 paulson 1999-02-03 tidied, with left_inverse & right_inverse as default simprules
1999-01-27 paulson 1999-01-27 new typechecking solver for the simplifier
1998-09-15 paulson 1998-09-15 tidied
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-08-06 paulson 1998-08-06 New results from AC
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-13 paulson 1998-07-13 Huge tidy-up: removal of leading \!\! addsplits split_tac[split_if] now default nat_succI now included by default
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-11-27 paulson 1997-11-27 Deleted some needless addSIs; got rid of a slow Blast_tac
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-29 paulson 1997-09-29 Much tidying including step_tac -> clarify_tac or safe_tac; sometimes used qed_spec_mp
1997-05-15 oheimb 1997-05-15 renamed unsafe_addss to addss
1997-04-09 paulson 1997-04-09 Using Blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-08 paulson 1997-01-08 Removal of sum_cs and eq_cs
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-06-07 paulson 1996-06-07 Addition of converse_iff, domain_converse, range_converse as rewrites
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-04-06 lcp 1995-04-06 Changed proof of domain_ord_iso_map_subset for new hyp_subst_tac
1995-03-31 lcp 1995-03-31 Tried the new addss in many proofs, and tidied others involving simplification.
1995-01-11 lcp 1995-01-11 Proved ord_isoI, ord_iso_refl. Simplified proof of ord_iso_restrict_pred. Proved theorems irrefl_0, ..., well_ord_0.
1994-12-23 lcp 1994-12-23 Added Krzysztof's theorems irrefl_converse, trans_on_converse, part_ord_converse, linear_converse, tot_ord_converse, Proved rvimage_converse, ord_iso_rvimage_eq
1994-12-20 lcp 1994-12-20 Simplified proof of ord_iso_image_pred using bij_inverse_ss. Replaced not_well_ord_iso_pred_lemma by much simpler well_ord_iso_subset_lemma. Simplifed proof of well_ord_iso_unique_lemma using well_ord_iso_subset_lemma.
1994-12-16 lcp 1994-12-16 moved congruence rule conj_cong2 to FOL/IFOL.ML
1994-12-14 lcp 1994-12-14 well_ord_iso_predE replaces not_well_ord_iso_pred well_ord_iso_unique: eliminated a premise using well_ord_ord_iso Proved well_ord_iso_pred_eq, ord_iso_image_pred, ord_iso_restrict_pred, part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso, well_ord_ord_iso, well_ord_iso_preserving, mono_map_is_fun, mono_map_is_inj, mono_map_trans, mono_ord_isoI, well_ord_mono_ord_isoI, ord_iso_is_mono_map, ord_iso_map_mono_map, ord_iso_map_ord_iso, domain_ord_iso_map_subset, domain_ord_iso_map_cases, range_ord_iso_map_cases, well_ord_trichotomy deleted bij_ss in favour of bij_inverse_ss
1994-12-14 clasohm 1994-12-14 added bind_thm for theorems defined by "standard ..."
1994-12-08 lcp 1994-12-08 not_well_ord_iso_pred: removed needless quantifier
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-07-26 lcp 1994-07-26 Axiom of choice, cardinality results, etc.
1994-07-12 lcp 1994-07-12 new cardinal arithmetic developments
1994-06-23 lcp 1994-06-23 modifications for cardinal arithmetic
1994-06-21 lcp 1994-06-21 Addition of cardinals and order types, various tidying