Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Code_Index.thy
changeset 26304 02fbd0e7954a
parent 26264 89e25cc8da7a
child 27104 791607529f6d 
--- a/src/HOL/Library/Code_Index.thy	Mon Mar 17 18:37:04 2008 +0100
+++ b/src/HOL/Library/Code_Index.thy	Mon Mar 17 18:37:05 2008 +0100
@@ -45,7 +45,7 @@
   shows P
   by (rule assms [of "nat_of_index k"]) simp
 
-lemma index_induct:
+lemma index_induct_raw:
   assumes "\<And>n. P (index_of_nat n)"
   shows "P k"
 proof -
isabelle