Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changed case names of converse_rtranclp_induct.
authorberghofe
Sun, 10 Jan 2010 18:37:37 +0100
changeset 34912 c04747153bcf
parent 34911 771830d3bd5e
child 34913 d8cb720c9c53
Changed case names of converse_rtranclp_induct.
src/HOL/Library/Transitive_Closure_Table.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle