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 41842 d8f76db6a207
parent 37667 41acc0fa6b6c
child 44939 5930d35c976d 
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 25 08:46:52 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 25 14:25:41 2011 +0100
@@ -308,12 +308,7 @@
    apply clarsimp
   apply clarsimp
   apply (case_tac w rule: bin_exhaust)
-  apply clarsimp
-  apply (case_tac "n - m")
-   apply arith
   apply simp
-  apply (rule_tac f = "%n. bl ! n" in arg_cong) 
-  apply arith
   done
   
 lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
isabelle