| changeset 61798 | 27f3c10b0b50 |
| parent 60770 | 240563fbf41d |
| child 65449 | c82e63b11b8b |
--- a/src/ZF/Induct/ListN.thy Mon Dec 07 10:19:30 2015 +0100 +++ b/src/ZF/Induct/ListN.thy Mon Dec 07 10:23:50 2015 +0100 @@ -8,7 +8,7 @@ theory ListN imports Main begin text \<open> - Inductive definition of lists of @{text n} elements; see + Inductive definition of lists of \<open>n\<close> elements; see @{cite "paulin-tlca"}. \<close>