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/Bool_List_Representation.thy
changeset 58410 6d46ad54a2ab
parent 57514 bdc2c6b40bf2
child 58874 7172c7ffb047 
--- a/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Sun Sep 21 16:56:11 2014 +0200
@@ -105,8 +105,8 @@
   by (cases n) auto
 
 lemma bin_to_bl_aux_minus1_minus_simp [simp]:
-  "0 < n ==> bin_to_bl_aux n -1 bl = 
-    bin_to_bl_aux (n - 1) -1 (True # bl)"
+  "0 < n ==> bin_to_bl_aux n (- 1) bl = 
+    bin_to_bl_aux (n - 1) (- 1) (True # bl)"
   by (cases n) auto
 
 lemma bin_to_bl_aux_one_minus_simp [simp]:
@@ -206,10 +206,10 @@
   unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
 
 lemma bin_to_bl_minus1_aux:
-  "bin_to_bl_aux n -1 bl = replicate n True @ bl"
+  "bin_to_bl_aux n (- 1) bl = replicate n True @ bl"
   by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
 
-lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
+lemma bin_to_bl_minus1: "bin_to_bl n (- 1) = replicate n True"
   unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
 
 lemma bl_to_bin_rep_F:
isabelle