# HG changeset patch
# User nipkow
# Date 1312781742 -7200
# Node ID 64f574163ca2b0c3df871bb16a6f8597ed12be7c
# Parent  18a0aef2af808289f7b16921ba4c682fc117fd65
removed old recdef and types usage

diff -r 18a0aef2af80 -r 64f574163ca2 doc-src/TutorialI/Types/Numbers.thy
--- 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{*
diff -r 18a0aef2af80 -r 64f574163ca2 doc-src/TutorialI/Types/document/Numbers.tex
--- 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}}}
diff -r 18a0aef2af80 -r 64f574163ca2 doc-src/TutorialI/fp.tex
--- 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}