doc-src/Tutorial/Ifexpr/boolex
author paulson
Fri, 21 May 1999 10:47:07 +0200
changeset 6674 32892a8ecb15
parent 5377 efb799c5ed3c
permissions -rw-r--r--
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5377
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     1
datatype boolex = Const bool | Var nat
efb799c5ed3c *** empty log message ***
nipkow
parents:
diff changeset
     2
                | Neg boolex | And boolex boolex