doc-src/TutorialI/Misc/document/fakenat.tex
changeset 48536 4e2ee88276d2
parent 48535 619531d87ce4
parent 48528 784c6f63d79c
child 48537 ba0dd46b9214
--- a/doc-src/TutorialI/Misc/document/fakenat.tex	Thu Jul 26 16:08:16 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{fakenat}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-\noindent
-The type \tydx{nat} of natural
-numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}.  It  behaves as if it were declared like this:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{datatype}\isamarkupfalse%
-\ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: