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.
Replaced application of subst by simplesubst in proof of rev_induct
authorberghofe
Wed, 02 Feb 2005 18:19:43 +0100
changeset 15489 d136af442665
parent 15488 7c638a46dcbb
child 15490 2a183ef25fb1
Replaced application of subst by simplesubst in proof of rev_induct to avoid problems with program extraction.
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Wed Feb 02 18:06:25 2005 +0100
+++ b/src/HOL/List.thy	Wed Feb 02 18:19:43 2005 +0100
@@ -582,7 +582,7 @@
 
 lemma rev_induct [case_names Nil snoc]:
   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(subst rev_rev_ident[symmetric])
+apply(simplesubst rev_rev_ident[symmetric])
 apply(rule_tac list = "rev xs" in list.induct, simp_all)
 done
isabelle