--- a/doc-src/ProgProve/Thys/document/Logic.tex Mon Apr 02 21:26:46 2012 +0100
+++ b/doc-src/ProgProve/Thys/document/Logic.tex Tue Apr 03 08:55:06 2012 +0200
@@ -570,7 +570,7 @@
\ ev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
ev{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}ev\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
evSS{\isaliteral{3A}{\isacharcolon}}\ \ %
-\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}
+\isa{{\isaliteral{22}{\isachardoublequote}}ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}
%
\begin{isamarkuptext}%
To get used to inductive definitions, we will first prove a few