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/Bit_Representation.thy
changeset 46025 64a19ea435fc
parent 46023 fad87bb608fc
parent 46008 c296c75f4cf4
child 46598 fd0ac848140e 
--- a/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 20:05:52 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy	Wed Dec 28 22:08:44 2011 +0100
@@ -235,14 +235,14 @@
     apply safe
     apply (erule rev_mp)
     apply (induct_tac y rule: bin_induct)
-      apply (safe del: subset_antisym)
+      apply safe
       apply (drule_tac x=0 in fun_cong, force)
      apply (erule notE, rule ext, 
             drule_tac x="Suc x" in fun_cong, force)
     apply (drule_tac x=0 in fun_cong, force simp: BIT_simps)
    apply (erule rev_mp)
    apply (induct_tac y rule: bin_induct)
-     apply (safe del: subset_antisym)
+     apply safe
      apply (drule_tac x=0 in fun_cong, force)
     apply (erule notE, rule ext, 
            drule_tac x="Suc x" in fun_cong, force)
isabelle