--- a/doc-src/TutorialI/Types/Numbers.thy Mon Aug 08 07:13:16 2011 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy Mon Aug 08 07:35:42 2011 +0200
@@ -16,8 +16,7 @@
*};
oops
-consts h :: "nat \<Rightarrow> nat"
-recdef h "{}"
+fun h :: "nat \<Rightarrow> nat" where
"h i = (if i = 3 then 2 else i)"
text{*
--- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 08 07:13:16 2011 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 08 07:35:42 2011 +0200
@@ -64,10 +64,8 @@
\endisadelimproof
\isanewline
\isanewline
-\isacommand{consts}\isamarkupfalse%
-\ h\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{recdef}\isamarkupfalse%
-\ h\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isacommand{fun}\isamarkupfalse%
+\ h\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}h\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\isa{h\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}}
--- a/doc-src/TutorialI/fp.tex Mon Aug 08 07:13:16 2011 +0200
+++ b/doc-src/TutorialI/fp.tex Mon Aug 08 07:35:42 2011 +0200
@@ -249,7 +249,7 @@
\index{type synonyms}%
Type synonyms are similar to those found in ML\@. They are created by a
-\commdx{types} command:
+\commdx{type\_synonym} command:
\medskip
\input{Misc/document/types.tex}