| changeset 16417 | 9bc16273c2d4 |
| parent 13111 | 2d6782e71702 |
| child 40878 | 7695e4de4d86 |
--- a/doc-src/TutorialI/Recdef/Nested2.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/doc-src/TutorialI/Recdef/Nested2.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,5 +1,5 @@ (*<*) -theory Nested2 = Nested0: +theory Nested2 imports Nested0 begin (*>*) lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"