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/Word/Ancient_Numeral.thy
changeset 72000 379d0c207c29
parent 71991 8bff286878bf
child 72010 a851ce626b78
equal deleted inserted replaced
71999:720b72513ae5 72000:379d0c207c29 
     1 theory Ancient_Numeral
 
     1 theory Ancient_Numeral
 
     2   imports Main Bits_Int
 
     2   imports Main Bits_Int Misc_lsb Misc_msb
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
 
     5 definition Bit :: "int \<Rightarrow> bool \<Rightarrow> int"  (infixl "BIT" 90)
 
     6   where "k BIT b = (if b then 1 else 0) + k + k"
 
     6   where "k BIT b = (if b then 1 else 0) + k + k"
 
     7 
     7
isabelle