changeset 10386 | 581a5a143994 |
parent 10261 | bb2f1e859177 |
child 10519 | ade64af4c57c |
--- a/src/HOL/Main.thy Fri Nov 03 21:32:41 2000 +0100 +++ b/src/HOL/Main.thy Fri Nov 03 21:33:15 2000 +0100 @@ -7,5 +7,7 @@ (*belongs to theory List*) declare lists_mono [mono] declare map_cong [recdef_cong] +lemmas rev_induct [case_names Nil snoc] = rev_induct + and rev_cases [case_names Nil snoc] = rev_exhaust end