src/HOL/Nominal/nominal_primrec.ML
Mon, 27 Nov 2006 12:10:51 +0100 berghofe Implemented new "nominal_primrec" command for defining
less more (0) tip