src/HOL/IOA/meta_theory/IOA.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 Removed commands made redundant by new one-point rules
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-06-28 paulson 1996-06-28 Removed a use of eq_cs
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets
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