equal
deleted
inserted
replaced
73 This style of \texttt{instance} won't make much sense in Isabelle's |
73 This style of \texttt{instance} won't make much sense in Isabelle's |
74 meta-logic, because there is no internal notion of ``providing |
74 meta-logic, because there is no internal notion of ``providing |
75 operations'' or even ``names of functions''.% |
75 operations'' or even ``names of functions''.% |
76 \end{isamarkuptext}% |
76 \end{isamarkuptext}% |
77 \isacommand{end}\end{isabelle}% |
77 \isacommand{end}\end{isabelle}% |
|
78 %%% Local Variables: |
|
79 %%% mode: latex |
|
80 %%% TeX-master: "root" |
|
81 %%% End: |