src/ZF/Finite.ML
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-05 paulson 1996-09-05 Renaming of _rews to _simps
1996-01-30 clasohm 1996-01-30 expanded tabs
1994-12-16 lcp 1994-12-16 changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results.
1994-12-07 clasohm 1994-12-07 added qed and qed_goal[w]
1994-08-16 lcp 1994-08-16 ZF/Finite: added the finite function space, A-||>B ZF/InfDatatype: added rules for the above
1994-08-12 lcp 1994-08-12 installation of new inductive/datatype sections