src/ZF/arith.thy
1993-11-16 clasohm made pseudo theories for all ML files;
1993-10-05 lcp ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
1993-09-17 lcp Installation of new simplifier for ZF. Deleted all congruence rules not
1993-09-16 clasohm Initial revision
less more (0) tip