equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline |
3 \isacommand{types}\ number\ \ \ \ \ \ \ {\isacharequal}\ nat\isanewline |
3 \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
4 \ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isachardoublequote}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
4 \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}% |
5 \ \ \ \ \ \ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}alist\ {\isacharequal}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isacharasterisk}\ {\isacharprime}b{\isacharparenright}list{\isachardoublequote}% |
5 \begin{isamarkuptext}% |
6 \begin{isamarkuptext}% |
6 \noindent\indexbold{*types}% |
7 \noindent\indexbold{*types}% |
36 \begin{isamarkuptext}% |
37 \begin{isamarkuptext}% |
37 \noindent\indexbold{*constdefs}% |
38 \noindent\indexbold{*constdefs}% |
38 in which case the default name of each definition is \isa{$f$_def}, where |
39 in which case the default name of each definition is \isa{$f$_def}, where |
39 $f$ is the name of the defined constant.% |
40 $f$ is the name of the defined constant.% |
40 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
41 \end{isabelle}% |
42 \end{isabellebody}% |
42 %%% Local Variables: |
43 %%% Local Variables: |
43 %%% mode: latex |
44 %%% mode: latex |
44 %%% TeX-master: "root" |
45 %%% TeX-master: "root" |
45 %%% End: |
46 %%% End: |