src/CTT/ex/elim.ML
1996-01-20 paulson 1996-01-20 Ran expandshort
1994-03-17 lcp 1994-03-17 CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD h:X.Y to fix the variable name h:X.
1993-09-16 clasohm 1993-09-16 Initial revision