Tue, 16 Jan 2001 00:25:00 +0100
changeset 10902 0f512daadbd5
parent 10901 bf131ef38495
child 10903 ad1fb17361e4
--- a/doc-src/TutorialI/Types/Pairs.thy	Tue Jan 16 00:24:36 2001 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy	Tue Jan 16 00:25:00 2001 +0100
@@ -71,7 +71,7 @@
 first place, we quickly realize that what we would like is to replace @{term
 p} with some concrete pair @{term"(a,b)"}, in which case both sides of the
 equation would simplify to @{term a} because of the simplification rules
-@{thm Product_Type.split[no_vars]} and @{thm fst_conv[no_vars]}.  This is the
+@{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}.  This is the
 key problem one faces when reasoning about pattern matching with pairs: how to
 convert some atomic term into a pair.