--- 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(*>*)
--- 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
*}
--- 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
--- 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%