# HG changeset patch
# User wenzelm
# Date 979601100 -3600
# Node ID 0f512daadbd5a7b8d8a13f5000d7bbfa84a6f75b
# Parent  bf131ef38495783f6558f64bc103e4ebf0072fb2
split_conv;

diff -r bf131ef38495 -r 0f512daadbd5 doc-src/TutorialI/Types/Pairs.thy
--- 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.