src/HOL/IOA/meta_theory/Solve.ML
1997-01-17 paulson 1997-01-17 New miniscoping rules for the bounded quantifiers and UN/INT operators
1996-10-07 paulson 1996-10-07 New proof required by change to simpdata.ML
1996-09-24 nipkow 1996-09-24 Moved Option into core HOL which caused a few local changes.
1996-09-05 paulson 1996-09-05 Simplified some proofs for compatibility with miniscoping
1996-07-30 berghofe 1996-07-30 Classical tactics now use default claset.
1996-04-19 clasohm 1996-04-19 adapted to new version of Fun.ML
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-04-13 nipkow 1995-04-13 Olafs new version.
1995-03-24 clasohm 1995-03-24 changed syntax of tuples from <..., ...> to (..., ...)
1995-03-20 clasohm 1995-03-20 converted IOA with curried function application