equal
deleted
inserted
replaced
47 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about |
47 \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}} when inverse is not defined on lists. Proving theorems about |
48 unspecified constants does not endanger soundness, but it is pointless. |
48 unspecified constants does not endanger soundness, but it is pointless. |
49 To prevent such terms from even being formed requires the use of type classes.% |
49 To prevent such terms from even being formed requires the use of type classes.% |
50 \end{isamarkuptext}% |
50 \end{isamarkuptext}% |
51 \isamarkuptrue% |
51 \isamarkuptrue% |
52 \isanewline |
|
53 \isamarkupfalse% |
52 \isamarkupfalse% |
54 \end{isabellebody}% |
53 \end{isabellebody}% |
55 %%% Local Variables: |
54 %%% Local Variables: |
56 %%% mode: latex |
55 %%% mode: latex |
57 %%% TeX-master: "root" |
56 %%% TeX-master: "root" |