--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Wed May 25 09:04:24 2005 +0200
@@ -100,10 +100,17 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+The proof is canonical:%
+\end{isamarkuptxt}%
\isamarkuptrue%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
%
\begin{isamarkuptext}%
\noindent
@@ -152,11 +159,9 @@
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -184,11 +189,9 @@
\isamarkuptrue%
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -217,21 +220,17 @@
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\isamarkupfalse%
-\isanewline
-\isamarkupfalse%
-\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex