# HG changeset patch
# User berghofe
# Date 1263145057 -3600
# Node ID c04747153bcf35c99c24943a8d211d1b5f09d142
# Parent  771830d3bd5e1107b4ab96218b74337c267c9ed9
Changed case names of converse_rtranclp_induct.

diff -r 771830d3bd5e -r c04747153bcf src/HOL/Library/Transitive_Closure_Table.thy
--- a/src/HOL/Library/Transitive_Closure_Table.thy	Sun Jan 10 18:11:00 2010 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Sun Jan 10 18:37:37 2010 +0100
@@ -17,11 +17,11 @@
   assume "r\<^sup>*\<^sup>* x y"
   then show "\<exists>xs. rtrancl_path r x xs y"
   proof (induct rule: converse_rtranclp_induct)
-    case 1
+    case base
     have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
     then show ?case ..
   next
-    case (2 x z)
+    case (step x z)
     from `\<exists>xs. rtrancl_path r z xs y`
     obtain xs where "rtrancl_path r z xs y" ..
     with `r x z` have "rtrancl_path r x (z # xs) y"