equal
deleted
inserted
replaced
9 imports BNF_Least_Fixpoint Old_Datatype |
9 imports BNF_Least_Fixpoint Old_Datatype |
10 begin |
10 begin |
11 |
11 |
12 subsection {* The @{text num} type *} |
12 subsection {* The @{text num} type *} |
13 |
13 |
14 datatype num = One | Bit0 num | Bit1 num |
14 datatype_new num = One | Bit0 num | Bit1 num |
15 |
15 |
16 text {* Increment function for type @{typ num} *} |
16 text {* Increment function for type @{typ num} *} |
17 |
17 |
18 primrec inc :: "num \<Rightarrow> num" where |
18 primrec inc :: "num \<Rightarrow> num" where |
19 "inc One = Bit0 One" | |
19 "inc One = Bit0 One" | |