src/HOL/Library/Multiset.thy
changeset 11868 56db9f3a6b3e
parent 11701 3d51fbf81c17
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -274,18 +274,8 @@
     1.4    apply (simp (no_asm) add: expand_fun_eq)
     1.5    apply (rule conjI)
     1.6     apply force
     1.7 -  apply clarify
     1.8 -  apply (rule conjI)
     1.9 -   apply blast
    1.10 -  apply clarify
    1.11 -  apply (rule iffI)
    1.12 -   apply (rule conjI)
    1.13 -    apply clarify
    1.14 -    apply (rule conjI)
    1.15 -     apply (simp add: eq_sym_conv)   (* FIXME blast fails !? *)
    1.16 -    apply fast
    1.17 -   apply simp
    1.18 -  apply force
    1.19 +  apply safe
    1.20 +  apply (simp_all add: eq_sym_conv)
    1.21    done
    1.22  
    1.23  (*