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.
recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
authorwenzelm
Sat, 04 Aug 2018 16:21:25 +0200
changeset 68723 60611540bcff
parent 68722 6aea897bff2a
child 68724 7fafadbf16c7
recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
src/HOL/List.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/List.thy	Sat Aug 04 15:49:54 2018 +0200
+++ b/src/HOL/List.thy	Sat Aug 04 16:21:25 2018 +0200
@@ -1242,7 +1242,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