Mercurial Mercurial > repos > isabelle / comparison
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.thy
changeset 41282 a4d1b5eef12e
parent 40513 1204d268464f
child 41601 fda8511006f9
equal deleted inserted replaced
41281:679118e35378 41282:a4d1b5eef12e 
    64 
    64 
    65 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
 
    65 lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by smt
 
    66 
    66 
    67 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
 
    67 lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by smt
 
    68 
    68 
    69 lemma "0b10011 << 2 = (0b1001100::8 word)" sorry (* FIXME *)
 
    69 lemma "0b10011 << 2 = (0b1001100::8 word)" by smt
 
    70 
    70 
    71 lemma "0b11001 >> 2 = (0b110::8 word)" sorry (* FIXME *)
 
    71 lemma "0b11001 >> 2 = (0b110::8 word)" by smt
 
    72 
    72 
    73 lemma "0b10011 >>> 2 = (0b100::8 word)" sorry (* FIXME *)
 
    73 lemma "0b10011 >>> 2 = (0b100::8 word)" by smt
 
    74 
    74 
    75 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
 
    75 lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by smt
 
    76 
    76 
    77 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
 
    77 lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by smt
 
    78 
    78
isabelle