equal
deleted
inserted
replaced
11 by(case_tac xs, simp, simp); |
11 by(case_tac xs, simp, simp); |
12 |
12 |
13 text{*\noindent |
13 text{*\noindent |
14 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a |
14 Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a |
15 sequence of methods. Assuming that the simplification rule |
15 sequence of methods. Assuming that the simplification rule |
16 *}(*<*)term(*>*) "(rev xs = []) = (xs = [])"; |
16 @{term"(rev xs = []) = (xs = [])"} |
17 text{*\noindent |
|
18 is present as well, |
17 is present as well, |
19 *} |
18 *} |
20 |
19 |
21 lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"; |
20 lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"; |
22 (*<*) |
21 (*<*) |