| changeset 35416 | d8d7d1b785af |
| parent 35216 | 7641e8d831d2 |
| child 35633 | 5da59c1ddece |
| 35342:4dc65845eab3 | 35416:d8d7d1b785af |
|---|---|
43 |
43 |
44 typedef (open Nat) |
44 typedef (open Nat) |
45 nat = Nat |
45 nat = Nat |
46 by (rule exI, unfold mem_def, rule Nat.Zero_RepI) |
46 by (rule exI, unfold mem_def, rule Nat.Zero_RepI) |
47 |
47 |
48 constdefs |
48 definition Suc :: "nat => nat" where |
49 Suc :: "nat => nat" |
|
50 Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
49 Suc_def: "Suc == (%n. Abs_Nat (Suc_Rep (Rep_Nat n)))" |
51 |
50 |
52 local |
51 local |
53 |
52 |
54 instantiation nat :: zero |
53 instantiation nat :: zero |