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.
doc-src/Tutorial/fp.tex
changeset 9721 7e51c9f3d5a0
parent 9676 4a3c49420efd 
--- a/doc-src/Tutorial/fp.tex	Tue Aug 29 12:28:48 2000 +0200
+++ b/doc-src/Tutorial/fp.tex	Tue Aug 29 15:13:10 2000 +0200
@@ -1029,7 +1029,7 @@
 Nevertheless the simplifier can be instructed to perform \texttt{case}-splits
 by adding the appropriate rule to the simpset:
 \begin{ttbox}
-by(simp_tac (simpset() addsplits [split_list_case]) 1);
+by(simp_tac (simpset() addsplits [list.split]) 1);
 \end{ttbox}\indexbold{*addsplits}
 solves the initial goal outright, which \texttt{Simp_tac} alone will not do.
isabelle