| changeset 58860 | fee7cfa69c50 |
| parent 48985 | 5386df44a037 |
| child 67406 | 23307fd33906 |
--- a/src/Doc/Tutorial/Misc/Tree2.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/Doc/Tutorial/Misc/Tree2.thy Sat Nov 01 14:20:38 2014 +0100 @@ -16,7 +16,7 @@ (*<*) lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs" apply(induct_tac t) -by(auto); +by(auto) (*>*) lemma "flatten2 t [] = flatten t" (*<*)