Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/Intro/gate.thy
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 105 216d6ed87399
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset 
     1
 
Gate = FOL +
216d6ed87399 Initial revision
lcp
parents:
diff changeset 
     2
 
consts  nand,xor :: "[o,o] => o"
216d6ed87399 Initial revision
lcp
parents:
diff changeset 
     3
 
rules   nand_def "nand(P,Q) == ~(P & Q)"
216d6ed87399 Initial revision
lcp
parents:
diff changeset 
     4
 
        xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
216d6ed87399 Initial revision
lcp
parents:
diff changeset 
     5
 
end
isabelle