author | berghofe |
Fri, 15 Oct 1999 15:31:35 +0200 | |
changeset 7872 | 2e2d7e80fb07 |
parent 7871 | 30fb773113a1 |
child 7873 | 5d1200c7a671 |
--- a/src/HOL/NatDef.thy Fri Oct 15 12:31:43 1999 +0200 +++ b/src/HOL/NatDef.thy Fri Oct 15 15:31:35 1999 +0200 @@ -64,7 +64,7 @@ Zero_def "0 == Abs_Nat(Zero_Rep)" Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))" - (*nat operations and recursion*) + (*nat operations*) pred_nat_def "pred_nat == {(m,n). n = Suc m}" less_def "m<n == (m,n):trancl(pred_nat)"