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.
src/HOL/SMT_Examples/SMT_Word_Examples.certs
author wenzelm
Tue, 03 Sep 2013 01:12:40 +0200
changeset 53374 a14d2a854c02
parent 50662 b1f4291eb916
child 54489 03ff4d1e6784
permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
     1
 
ef8166854c461e296fe9c596b7a3fe12065b0c65 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
     2
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
     3
 
d1ec4aa8c4a5f474e8dbb8a8acbdd12fc33b0cda 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
     4
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
     5
 
03dee604b20d98218bc88a69efcbf0f1c6dc057a 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
     6
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
     7
 
6a68bdb5b2a92a239021f6188a807622fe7b8213 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
     8
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
     9
 
9be3195f24c1786963c05e51e63a24efa7c83141 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    10
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    11
 
608ed753221bdf2f1769ea3686a0f970108a7087 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    12
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    13
 
610484e81fc38952a9a2cb0bfc83d424f7f96ca8 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    14
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    15
 
0a06a4c179bec3512f3dc01e338f246fca223ddb 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    16
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    17
 
dd232118189a55ac7fc80599d2738be8bbaa9333 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    18
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    19
 
8426f9081bd693e21cd8b2e13d07cea1e69e8abd 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    20
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    21
 
8d83ab1c5a55640d0165bbd736d2cc217bcc2efd 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    22
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    23
 
542ef8141028455b42a51f60e3981a74373a60b3 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    24
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    25
 
564709a03da50b938c3b1ab2a8a2f0dc8d8a4749 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    26
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    27
 
c4acaeb4324634878481e3faae3beae53a641067 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    28
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    29
 
873ce0289bcfaf43a446c6ed55bec4289eea0ffd 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    30
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    31
 
8383b80b5e8011f2b51c01ea89c14ce766f5a82b 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    32
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    33
 
6694dc1c5420588e5e48281a8835ac019bfb1aa7 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    34
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    35
 
4094196f5d25f48682e6634b4326469abc38d250 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    36
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    37
 
0597f614ff89c7376d01987b4737ab991b5a321c 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    38
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    39
 
44f955a3f3fab3f5203ec29edc7e00e7cb81bedc 1 0
41282
a4d1b5eef12e updated SMT certificates
boehmes
parents: 41132
diff changeset 
    40
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    41
 
927e5f0e88fadf6d2f604b1d863a37fc682f942b 1 0
41282
a4d1b5eef12e updated SMT certificates
boehmes
parents: 41132
diff changeset 
    42
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    43
 
818922160b53f843888d258a1ef7e5d5ddf5129f 1 0
41282
a4d1b5eef12e updated SMT certificates
boehmes
parents: 41132
diff changeset 
    44
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    45
 
afc6dff121c48475665b0ef064826ffa2cad0e85 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    46
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    47
 
b9ab61d9521faeaa45ec63bff4581742c3e6c550 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    48
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    49
 
8e60769fce6622cdca312aa54d4a77329a99dac2 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    50
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    51
 
bd55726cefc783f8e9ef4ad38596e1f24cca3663 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    52
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    53
 
4e48efd5c9874aedf200e06875d5597b31d98075 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    54
 
unsat
50662
b1f4291eb916 regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs
blanchet
parents: 49995
diff changeset 
    55
 
e5c27ae0a583eeafeaa4ef3c59b1b4ec53e06b0f 1 0
36900
631e961a9e95 updated SMT certificates
boehmes
parents:
diff changeset 
    56
 
unsat
isabelle