equal
deleted
inserted
replaced
4 ~~~~~~('a,'b)alist~=~{"}('a~*~'b)list{"}% |
4 ~~~~~~('a,'b)alist~=~{"}('a~*~'b)list{"}% |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \noindent\indexbold{*types}% |
6 \noindent\indexbold{*types}% |
7 Internally all synonyms are fully expanded. As a consequence Isabelle's |
7 Internally all synonyms are fully expanded. As a consequence Isabelle's |
8 output never contains synonyms. Their main purpose is to improve the |
8 output never contains synonyms. Their main purpose is to improve the |
9 readability of theory definitions. Synonyms can be used just like any other |
9 readability of theories. Synonyms can be used just like any other |
10 type:% |
10 type:% |
11 \end{isamarkuptext}% |
11 \end{isamarkuptext}% |
12 \isacommand{consts}~nand~::~gate\isanewline |
12 \isacommand{consts}~nand~::~gate\isanewline |
13 ~~~~~~~exor~::~gate% |
13 ~~~~~~~exor~::~gate% |
14 \begin{isamarkuptext}% |
14 \begin{isamarkuptext}% |
22 \isacommand{defs}~nand\_def:~{"}nand~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymand}~B){"}\isanewline |
22 \isacommand{defs}~nand\_def:~{"}nand~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymand}~B){"}\isanewline |
23 ~~~~~exor\_def:~{"}exor~A~B~{\isasymequiv}~A~{\isasymand}~{\isasymnot}B~{\isasymor}~{\isasymnot}A~{\isasymand}~B{"}% |
23 ~~~~~exor\_def:~{"}exor~A~B~{\isasymequiv}~A~{\isasymand}~{\isasymnot}B~{\isasymor}~{\isasymnot}A~{\isasymand}~B{"}% |
24 \begin{isamarkuptext}% |
24 \begin{isamarkuptext}% |
25 \noindent% |
25 \noindent% |
26 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and |
26 where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and |
27 \isa{exor_def} are arbitrary user-supplied names. |
27 \isa{exor_def} are user-supplied names. |
28 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
28 The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality |
29 that should only be used in constant definitions. |
29 that should only be used in constant definitions. |
30 Declarations and definitions can also be merged% |
30 Declarations and definitions can also be merged% |
31 \end{isamarkuptext}% |
31 \end{isamarkuptext}% |
32 \isacommand{constdefs}~nor~::~gate\isanewline |
32 \isacommand{constdefs}~nor~::~gate\isanewline |