equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 section \<open>Small Concrete Examples\<close> |
9 section \<open>Small Concrete Examples\<close> |
10 |
10 |
11 theory Small_Concrete |
11 theory Small_Concrete |
12 imports "~~/src/HOL/Library/BNF_Corec" |
12 imports "HOL-Library.BNF_Corec" |
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Streams of Natural Numbers\<close> |
15 subsection \<open>Streams of Natural Numbers\<close> |
16 |
16 |
17 codatatype natstream = S (head: nat) (tail: natstream) |
17 codatatype natstream = S (head: nat) (tail: natstream) |