src/HOL/Hoare/hoare_tac.ML
changeset 26300 03def556e26e
parent 24475 a297ae4ff188
child 27244 af0a44372d1f
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:36:04 2008 +0100
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:37:00 2008 +0100
     1.3 @@ -86,15 +86,10 @@
     1.4  (** input does not suffer any unexpected transformation                     **)
     1.5  (*****************************************************************************)
     1.6  
     1.7 -Goal "-(Collect b) = {x. ~(b x)}";
     1.8 -by (Fast_tac 1);
     1.9 -qed "Compl_Collect";
    1.10 -
    1.11 -
    1.12  (**Simp_tacs**)
    1.13  
    1.14  val before_set2pred_simp_tac =
    1.15 -  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
    1.16 +  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
    1.17  
    1.18  val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
    1.19