src/HOL/Sexp.ML
1998-08-06 paulson 1998-08-06 even more tidying of Goal commands
1998-07-24 berghofe 1998-07-24 Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1998-01-08 paulson 1998-01-08 Tidied by adding more default simprules
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-04-24 paulson 1997-04-24 A bit of tidying
1997-04-04 paulson 1997-04-04 Calls Blast_tac. Tidied some proofs
1996-10-10 paulson 1996-10-10 Deleted obsolete clasets
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
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-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-03 clasohm 1995-03-03 new version of HOL with curried function application