equal
deleted
inserted
replaced
8 theory Abstract_NAT |
8 theory Abstract_NAT |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *} |
12 text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *} |
|
13 |
|
14 hide (open) const succ |
13 |
15 |
14 locale NAT = |
16 locale NAT = |
15 fixes zero :: 'n |
17 fixes zero :: 'n |
16 and succ :: "'n \<Rightarrow> 'n" |
18 and succ :: "'n \<Rightarrow> 'n" |
17 assumes succ_inject [simp]: "(succ m = succ n) = (m = n)" |
19 assumes succ_inject [simp]: "(succ m = succ n) = (m = n)" |