src/HOL/WF_Rel.ML
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-16 paulson 2000-06-16 renamed psubset_card -> psubset_card_mono
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-03-22 paulson 2000-03-22 made a proof more robust (did not like Suc_less_eq)
2000-02-18 paulson 2000-02-18 expandshort
2000-01-28 oheimb 2000-01-28 added full_nat_induct
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-06-09 nipkow 1999-06-09 Stefan Merz's lemmas.
1998-07-15 nipkow 1998-07-15 Minor tidying up.
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-03-24 oheimb 1998-03-24 added finite_acyclic_wf_converse: corrected 8bit chars
1998-03-24 oheimb 1998-03-24 added finite_acyclic_wf_converse
1998-02-22 nipkow 1998-02-22 New induction schemas for lists (length and snoc).
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-07-02 nipkow 1997-07-02 Added the following lemmas tp Divides and a few others to Arith and NatDef: div_le_mono, div_le_mono2, div_le_dividend, div_less_dividend Fixed a broken proof in WF_Rel.ML. No idea what caused this.
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-18 paulson 1997-06-18 Addition of not_imp (which pushes negation into implication) as a default simprule
1997-06-13 nipkow 1997-06-13 Tuned wf_iff_no_infinite_down_chain proof, based on Konrads ideas. Added selectI2EX.
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
1997-05-22 paulson 1997-05-22 Deleted rprod: lex_prod is (usually?) enough
1997-05-20 paulson 1997-05-20 Relation "less_than" internalizes "<" for easy use of TFL
1997-05-15 paulson 1997-05-15 New theories used by TFL