src/HOL/WF.ML
1998-08-19 paulson 1998-08-19 tidied
1998-08-18 paulson 1998-08-18 added comment
1998-08-14 paulson 1998-08-14 expandshort
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-08-08 nipkow 1998-08-08 List now contains some lexicographic orderings.
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-07-12 wenzelm 1998-07-12 isatool expandshort;
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-22 nipkow 1998-04-22 Modifications due to improved simplifier.
1998-03-30 oheimb 1998-03-30 added wf_converse_trancl, adapted proof of wfrec
1998-03-24 oheimb 1998-03-24 added acyclicI
1998-03-16 paulson 1998-03-16 inverse -> converse [It is standard terminology and also used in ZF]
1998-03-07 nipkow 1998-03-07 Removed `addsplits [expand_if]'
1997-12-03 paulson 1997-12-03 updated for latest Blast_tac, which treats equality differently
1997-11-05 paulson 1997-11-05 Ran expandshort, especially to introduce Safe_tac
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-17 nipkow 1997-10-17 setloop split_tac -> addsplits
1997-09-25 paulson 1997-09-25 Changed some proofs to use Clarify_tac
1997-06-23 paulson 1997-06-23 Ran expandshort
1997-06-17 nipkow 1997-06-17 converse -> ^-1
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-23 nipkow 1997-05-23 Added `arbitrary'
1997-05-15 paulson 1997-05-15 New proofs for TFL
1997-04-11 paulson 1997-04-11 Yet more fast_tac->blast_tac, and other tidying
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-29 nipkow 1996-05-29 Replaced setsolver by addsolver
1996-05-23 berghofe 1996-05-23 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.
1996-04-04 paulson 1996-04-04 Using new "Times" infix
1996-03-27 paulson 1996-03-27 Library changes for mutilated checkerboard
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-13 nipkow 1995-03-13 Removed superfluous type constraint
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application