Changed case names of converse_rtranclp_induct.
authorberghofe
Sun Jan 10 18:37:37 2010 +0100 (2010-01-10)
changeset 34912c04747153bcf
parent 34911 771830d3bd5e
child 34913 d8cb720c9c53
Changed case names of converse_rtranclp_induct.
src/HOL/Library/Transitive_Closure_Table.thy
     1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Sun Jan 10 18:11:00 2010 +0100
     1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Sun Jan 10 18:37:37 2010 +0100
     1.3 @@ -17,11 +17,11 @@
     1.4    assume "r\<^sup>*\<^sup>* x y"
     1.5    then show "\<exists>xs. rtrancl_path r x xs y"
     1.6    proof (induct rule: converse_rtranclp_induct)
     1.7 -    case 1
     1.8 +    case base
     1.9      have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
    1.10      then show ?case ..
    1.11    next
    1.12 -    case (2 x z)
    1.13 +    case (step x z)
    1.14      from `\<exists>xs. rtrancl_path r z xs y`
    1.15      obtain xs where "rtrancl_path r z xs y" ..
    1.16      with `r x z` have "rtrancl_path r x (z # xs) y"