# HG changeset patch
# User berghofe
# Date 1210150782 -7200
# Node ID a62f8db42f4a47ca5640878ec034578b4333594c
# Parent  fd8fdf21660f49235f0e40b4b2b5fac61fce44c2
Deleted subset_antisym in a few proofs, because it is
accidentally applied to predicates as well.

diff -r fd8fdf21660f -r a62f8db42f4a src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Wed May 07 10:59:41 2008 +0200
+++ b/src/HOL/Word/BinGeneral.thy	Wed May 07 10:59:42 2008 +0200
@@ -272,14 +272,14 @@
     apply safe
     apply (erule rev_mp)
     apply (induct_tac y rule: bin_induct)
-      apply safe
+      apply (safe del: subset_antisym)
       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)
    apply (erule rev_mp)
    apply (induct_tac y rule: bin_induct)
-     apply safe
+     apply (safe del: subset_antisym)
      apply (drule_tac x=0 in fun_cong, force)
     apply (erule notE, rule ext, 
            drule_tac x="Suc x" in fun_cong, force)
diff -r fd8fdf21660f -r a62f8db42f4a src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Wed May 07 10:59:41 2008 +0200
+++ b/src/HOL/Word/WordBitwise.thy	Wed May 07 10:59:42 2008 +0200
@@ -327,7 +327,7 @@
   "n = size (w::'a::len0 word) ==> ofn = set_bits ==> [w, ofn g] = l ==> 
     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
   apply (unfold word_size td_ext_def')
-  apply safe
+  apply (safe del: subset_antisym)
      apply (rule_tac [3] ext)
      apply (rule_tac [4] ext)
      apply (unfold word_size of_nth_def test_bit_bl)