# HG changeset patch
# User wenzelm
# Date 1208377063 -7200
# Node ID ca558202ffa5bccd1d3df996dc7cd3b67eaadd0e
# Parent  3b9eede406087fe0a6708511940d5fd1955860be
Sign.add_path;

diff -r 3b9eede40608 -r ca558202ffa5 doc-src/TutorialI/Documents/Documents.thy
--- a/doc-src/TutorialI/Documents/Documents.thy	Wed Apr 16 21:53:05 2008 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy	Wed Apr 16 22:17:43 2008 +0200
@@ -140,7 +140,7 @@
 
 (*<*)
 hide const xor
-setup {* Theory.add_path "version1" *}
+setup {* Sign.add_path "version1" *}
 (*>*)
 constdefs
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "\<oplus>" 60)
@@ -164,7 +164,7 @@
 
 (*<*)
 hide const xor
-setup {* Theory.add_path "version2" *}
+setup {* Sign.add_path "version2" *}
 (*>*)
 constdefs
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"    (infixl "[+]\<ignore>" 60)
diff -r 3b9eede40608 -r ca558202ffa5 doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Wed Apr 16 21:53:05 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Wed Apr 16 22:17:43 2008 +0200
@@ -104,7 +104,7 @@
 If we consider why this lemma presents a problem, 
 we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}.  Then both sides of the
 equation would simplify to \isa{a} by the simplification rules
-\isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.  
+\isa{split\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.  
 To reason about tuple patterns requires some way of
 converting a variable of product type into a pair.