# HG changeset patch
# User nipkow
# Date 1213273270 -7200
# Node ID 89d5f117add30ea826d2fcbce494d3047ea98461
# Parent  9a9cc62932d97db20de1d688258c94c168af31c2
fixed type

diff -r 9a9cc62932d9 -r 89d5f117add3 doc-src/TutorialI/Types/Overloading.thy
--- a/doc-src/TutorialI/Types/Overloading.thy	Thu Jun 12 14:20:52 2008 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy	Thu Jun 12 14:21:10 2008 +0200
@@ -14,7 +14,8 @@
 
 defs (overloaded)
 prefix_def:
-  "xs <<= (ys::'a::ordrel list)  \<equiv>  \<exists>zs. ys = xs@zs"
+  "xs <<= (ys::'a list)  \<equiv>  \<exists>zs. ys = xs@zs"
 strict_prefix_def:
-  "xs << (ys::'a::ordrel list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
+  "xs << (ys::'a list)   \<equiv>  xs <<= ys \<and> xs \<noteq> ys"
+
 (*<*)end(*>*)
diff -r 9a9cc62932d9 -r 89d5f117add3 doc-src/TutorialI/Types/Pairs.thy
--- a/doc-src/TutorialI/Types/Pairs.thy	Thu Jun 12 14:20:52 2008 +0200
+++ b/doc-src/TutorialI/Types/Pairs.thy	Thu Jun 12 14:21:10 2008 +0200
@@ -110,7 +110,7 @@
 @{subgoals[display,indent=0]}
 Again, simplification produces a term suitable for @{thm[source]split_split}
 as above. If you are worried about the strange form of the premise:
-@{term"split (op =)"} is short for @{text"\<lambda>(x,y). x=y"}.
+@{text"split (op =)"} is short for @{term"\<lambda>(x,y). x=y"}.
 The same proof procedure works for
 *}
 
diff -r 9a9cc62932d9 -r 89d5f117add3 doc-src/TutorialI/Types/document/Overloading.tex
--- a/doc-src/TutorialI/Types/document/Overloading.tex	Thu Jun 12 14:20:52 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex	Thu Jun 12 14:21:10 2008 +0200
@@ -44,9 +44,10 @@
 \isacommand{defs}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
 prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequoteclose}\isanewline
 strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}%
+\ \ {\isachardoublequoteopen}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequoteclose}\isanewline
+%
 \isadelimtheory
 %
 \endisadelimtheory
diff -r 9a9cc62932d9 -r 89d5f117add3 doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Thu Jun 12 14:20:52 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Thu Jun 12 14:21:10 2008 +0200
@@ -198,7 +198,7 @@
 \end{isabelle}
 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
 as above. If you are worried about the strange form of the premise:
-\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
+\isa{split\ {\isacharparenleft}op\ {\isacharequal}{\isacharparenright}} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y}.
 The same proof procedure works for%
 \end{isamarkuptxt}%
 \isamarkuptrue%