| changeset 67613 | ce654b0e6d69 |
| parent 67406 | 23307fd33906 |
| child 69505 | cc2d676d5395 |
--- a/src/Doc/Tutorial/Misc/Tree2.thy Tue Feb 13 14:24:50 2018 +0100 +++ b/src/Doc/Tutorial/Misc/Tree2.thy Thu Feb 15 12:11:00 2018 +0100 @@ -14,7 +14,7 @@ text\<open>\noindent and prove\<close> (*<*) -lemma [simp]: "!xs. flatten2 t xs = flatten t @ xs" +lemma [simp]: "\<forall>xs. flatten2 t xs = flatten t @ xs" apply(induct_tac t) by(auto) (*>*)