--- a/doc-src/TutorialI/Misc/document/types.tex Thu Jul 26 16:54:44 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{types}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
-\ number\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
-\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
-\ gate\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
-\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ alist\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ list{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-Internally all synonyms are fully expanded. As a consequence Isabelle's
-output never contains synonyms. Their main purpose is to improve the
-readability of theories. Synonyms can be used just like any other
-type.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Constant Definitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:ConstDefinitions}\indexbold{definitions}%
-Nonrecursive definitions can be made with the \commdx{definition}
-command, for example \isa{nand} and \isa{xor} gates
-(based on type \isa{gate} above):%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{definition}\isamarkupfalse%
-\ nand\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ gate\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}nand\ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\isacommand{definition}\isamarkupfalse%
-\ xor\ \ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ gate\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}xor\ \ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent%
-The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
-that must be used in constant definitions.
-Pattern-matching is not allowed: each definition must be of
-the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
-Section~\ref{sec:Simp-with-Defs} explains how definitions are used
-in proofs. The default name of each definition is $f$\isa{{\isaliteral{5F}{\isacharunderscore}}def}, where
-$f$ is the name of the defined constant.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: