src/HOL/SMT_Examples/SMT_Word_Examples.certs
author haftmann
Wed, 08 Dec 2010 13:34:50 +0100
changeset 41075 4bed56dc95fb
parent 41064 0c447a17770a
child 41132 42384824b732
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`

8feec88bda876aef49ce85ea346ff6a145eb2f84 1 0
unsat
48892a95f694eea9655c4ebcdf3d0673a2fda935 1 0
unsat
517aa41cf07ed4cc7725322f0d4f39f622c17c4b 1 0
unsat
2602a0bf08ddc272218686654070d5162cae3e47 1 0
unsat
12b9edc0b76c7a8a3a97507daa8b6e0ecf7d1f15 1 0
unsat
5fbd5c4f8b16cb89d1a52c3c741da789d6d71a9d 1 0
unsat
ae9cdca1e121299c88024fa354331a389bfa963e 1 0
unsat
2b0bd718f433d30e94db6efb1f294c1be486e5f7 1 0
unsat
dca62445470bae90ed728f82790f0eb807e48eaf 1 0
unsat
db7b59838473143aa075d5d7ea03cc2ef5d26c04 1 0
unsat
15cacc97b892b9c33df5d7a7bb4807dd7a9e74bd 1 0
unsat
321046a3dee3e14f71a92344cf53f3bc5c6f09c8 1 0
unsat
4b99cf8ccbd92279a6ff24af8cd6be5f67645891 1 0
unsat
7045c7b5b7367602e1b18b2f15ea85eba1575c2f 1 0
unsat
7ff5096d7461afdd27a32b9ae9f07f5bbb68f14e 1 0
unsat
e0834e363c8c1f0e94a8f90076afdbba0bd953e1 1 0
unsat
509c76346d27e3cbf1917884281422fa7e5eebe3 1 0
unsat
d3ebc96fbbafc5d776956f54971a6ba3ca64c24a 1 0
unsat
776c427e77f5c3599c361d086d1d797b93d4d9d3 1 0
unsat
f1501ae565b43d1019f299a4f3008fe7ec846342 1 0
unsat
18b124171d254c9e8dc87ab9d2665276ca0b7503 1 0
unsat
ad5538c5a8b7b9ce091f0cba5576cc03e920da17 1 0
unsat
028bd213a67b251c56208fadfb38a31937a84c53 1 0
unsat
c8b644947e686f276d8a787cf86849718b244212 1 0
unsat
f887fa7eb0486a214166b54ef46a7e0eacb6605b 1 0
unsat