src/HOL/intr_elim.ML
1997-02-28 paulson 1997-02-28 rule_by_tactic no longer standardizes its result
1996-12-16 paulson 1996-12-16 intro_tacsf: replaced ORELSE by APPEND in order to stop errors that arise when unconstrained equalities appear in the premises. Could cause runtimes to increase...
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-12-28 paulson 1995-12-28 Removed unfold:thm from signature INTR_ELIM and from the functor result. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store.
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-07-25 lcp 1995-07-25 Added two final lines to intro_tacsf for mutual recursion (borrowed from ZF version)
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application