doc-src/TutorialI/Types/document/Pairs.tex
changeset 15446 b022b72ccc03
parent 14387 e96d5c42c4b0
child 15481 fc075ae929e4
equal deleted inserted replaced
15445:8244894d0a41 15446:b022b72ccc03
   129 \begin{isabelle}%
   129 \begin{isabelle}%
   130 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p%
   130 \ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p%
   131 \end{isabelle}
   131 \end{isabelle}
   132 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
   132 Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
   133 as above. If you are worried about the strange form of the premise:
   133 as above. If you are worried about the strange form of the premise:
   134 \isa{split\ op\ {\isacharequal}} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
   134 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
   135 The same proof procedure works for%
   135 The same proof procedure works for%
   136 \end{isamarkuptxt}%
   136 \end{isamarkuptxt}%
   137 \isamarkuptrue%
   137 \isamarkuptrue%
   138 \isamarkupfalse%
   138 \isamarkupfalse%
   139 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%
   139 \isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%