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/BinBoolList.thy
changeset 26008 24c82bef5696
parent 25919 8b1c0d434824
child 26086 3c243098b64a 
--- a/src/HOL/Word/BinBoolList.thy	Mon Jan 28 22:27:27 2008 +0100
+++ b/src/HOL/Word/BinBoolList.thy	Mon Jan 28 22:27:29 2008 +0100
@@ -867,7 +867,7 @@
 lemma rbl_add_split: 
   "P (rbl_add (y # ys) (x # xs)) = 
     (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> 
-    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) & \ 
+    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) &
     (~ y --> P (x # ws)))"
   apply (auto simp add: Let_def)
    apply (case_tac [!] "y")
isabelle