Mercurial Mercurial > repos > isabelle / diff
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/Bits_Int.thy
changeset 58410 6d46ad54a2ab
parent 54874 c55c5dacd6a1
child 58874 7172c7ffb047 
--- a/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bits_Int.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -462,7 +462,7 @@
 lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
   by (induct n) auto
 
-lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
+lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
   by (induct n) auto
   
 lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -583,7 +583,7 @@
   by (induct n) auto
 
 lemma bin_split_minus1 [simp]:
-  "bin_split n -1 = (-1, bintrunc n -1)"
+  "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
   by (induct n) auto
 
 lemma bin_split_trunc:
isabelle