Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make uses of constant bin_sc respect int/bin distinction
authorhuffman
Thu, 23 Feb 2012 15:15:48 +0100
changeset 46608 37e383cc7831
parent 46607 6ae8121448af
child 46609 5cb607cb7651
make uses of constant bin_sc respect int/bin distinction
src/HOL/Word/Bit_Int.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Word/Bit_Int.thy	Thu Feb 23 15:04:51 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Thu Feb 23 15:15:48 2012 +0100
@@ -403,11 +403,11 @@
    apply (auto simp: le_Bits)
   done
 
-lemma bin_sc_FP [simp]: "bin_sc n 0 Int.Pls = Int.Pls"
-  by (induct n) (auto simp: BIT_simps)
+lemma bin_sc_FP [simp]: "bin_sc n 0 0 = 0"
+  by (induct n) auto
 
-lemma bin_sc_TM [simp]: "bin_sc n 1 Int.Min = Int.Min"
-  by (induct n) (auto simp: BIT_simps)
+lemma bin_sc_TM [simp]: "bin_sc n 1 -1 = -1"
+  by (induct n) auto
   
 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
isabelle