| changeset 12156 | d2758965362e |
| parent 11711 | ecdfd237ffee |
| child 16417 | 9bc16273c2d4 |
--- a/doc-src/TutorialI/Inductive/Advanced.thy Mon Nov 12 10:44:55 2001 +0100 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Mon Nov 12 10:56:38 2001 +0100 @@ -76,6 +76,7 @@ by (blast intro!: mono_Int monoI gterms_mono) +text{*the following declaration isn't actually used*} consts integer_arity :: "integer_op \<Rightarrow> nat" primrec "integer_arity (Number n) = 0"