equal
deleted
inserted
replaced
10 |
10 |
11 NatDef = Wellfounded_Recursion + |
11 NatDef = Wellfounded_Recursion + |
12 |
12 |
13 (** type ind **) |
13 (** type ind **) |
14 |
14 |
15 global |
15 types ind |
16 |
16 arities ind :: type |
17 types |
|
18 ind |
|
19 |
|
20 arities |
|
21 ind :: term |
|
22 |
17 |
23 consts |
18 consts |
24 Zero_Rep :: ind |
19 Zero_Rep :: ind |
25 Suc_Rep :: ind => ind |
20 Suc_Rep :: ind => ind |
26 |
21 |
40 |
35 |
41 inductive Nat' |
36 inductive Nat' |
42 intrs |
37 intrs |
43 Zero_RepI "Zero_Rep : Nat'" |
38 Zero_RepI "Zero_Rep : Nat'" |
44 Suc_RepI "i : Nat' ==> Suc_Rep i : Nat'" |
39 Suc_RepI "i : Nat' ==> Suc_Rep i : Nat'" |
|
40 |
|
41 global |
45 |
42 |
46 typedef (Nat) |
43 typedef (Nat) |
47 nat = "Nat'" (Nat'.Zero_RepI) |
44 nat = "Nat'" (Nat'.Zero_RepI) |
48 |
45 |
49 instance |
46 instance |