equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Fundata}% |
3 \def\isabellecontext{Fundata}% |
4 \isanewline |
|
5 \isamarkupfalse% |
4 \isamarkupfalse% |
6 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isamarkupfalse% |
5 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree\ {\isacharequal}\ Tip\ {\isacharbar}\ Br\ {\isacharprime}a\ {\isachardoublequote}{\isacharprime}i\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}i{\isacharparenright}bigtree{\isachardoublequote}\isamarkupfalse% |
7 % |
6 % |
8 \begin{isamarkuptext}% |
7 \begin{isamarkuptext}% |
9 \noindent |
8 \noindent |
44 \isamarkuptrue% |
43 \isamarkuptrue% |
45 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline |
44 \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline |
46 \isamarkupfalse% |
45 \isamarkupfalse% |
47 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
46 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline |
48 \isamarkupfalse% |
47 \isamarkupfalse% |
49 \isacommand{done}\isamarkupfalse% |
48 \isacommand{done}\isanewline |
|
49 \isamarkupfalse% |
50 \isamarkupfalse% |
50 \isamarkupfalse% |
51 \isamarkupfalse% |
51 \isamarkupfalse% |
52 % |
52 % |
53 \begin{isamarkuptxt}% |
53 \begin{isamarkuptxt}% |
54 \noindent |
54 \noindent |
60 \isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ }map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}% |
60 \isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ }map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}Br\ a\ F{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}Br\ a\ F{\isacharparenright}{\isacharparenright}% |
61 \end{isabelle}% |
61 \end{isabelle}% |
62 \end{isamarkuptxt}% |
62 \end{isamarkuptxt}% |
63 \isamarkuptrue% |
63 \isamarkuptrue% |
64 \isamarkupfalse% |
64 \isamarkupfalse% |
65 \isanewline |
|
66 \isamarkupfalse% |
65 \isamarkupfalse% |
67 \end{isabellebody}% |
66 \end{isabellebody}% |
68 %%% Local Variables: |
67 %%% Local Variables: |
69 %%% mode: latex |
68 %%% mode: latex |
70 %%% TeX-master: "root" |
69 %%% TeX-master: "root" |