--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Oct 01 20:13:32 2009 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Oct 01 20:20:45 2009 +0200
@@ -362,7 +362,7 @@
subgoal may look uninviting, but fortunately
\isa{lists} distributes over intersection:
\begin{isabelle}%
-lists\ {\isacharparenleft}A\ {\isasyminter}\ B{\isacharparenright}\ {\isacharequal}\ lists\ A\ {\isasyminter}\ lists\ B\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}%
+listsp\ {\isacharparenleft}{\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ B{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ A{\isacharparenright}\ {\isasyminter}\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ x\ {\isasymin}\ lists\ B{\isacharparenright}\rulename{lists{\isacharunderscore}Int{\isacharunderscore}eq}%
\end{isabelle}
Thanks to this default simplification rule, the induction hypothesis
is quickly replaced by its two parts: