equal
deleted
inserted
replaced
6 section \<open>Lists of n elements\<close> |
6 section \<open>Lists of n elements\<close> |
7 |
7 |
8 theory ListN imports Main begin |
8 theory ListN imports Main begin |
9 |
9 |
10 text \<open> |
10 text \<open> |
11 Inductive definition of lists of @{text n} elements; see |
11 Inductive definition of lists of \<open>n\<close> elements; see |
12 @{cite "paulin-tlca"}. |
12 @{cite "paulin-tlca"}. |
13 \<close> |
13 \<close> |
14 |
14 |
15 consts listn :: "i=>i" |
15 consts listn :: "i=>i" |
16 inductive |
16 inductive |