# HG changeset patch
# User wenzelm
# Date 973283595 -3600
# Node ID 581a5a143994a1c31aea9501d1a6a3205f1ec81d
# Parent  22836e4c5f4eb4bdef9c1c6a52188ab9a39db12d
provide case names for rev_induct, rev_cases;

diff -r 22836e4c5f4e -r 581a5a143994 src/HOL/Main.thy
--- 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