src/HOL/Hoare/hoare_tac.ML
changeset 27330 1af2598b5f7d
parent 27244 af0a44372d1f
child 28457 25669513fd4c
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -72,8 +72,7 @@
     1.4                           (Free ("P",varsT --> boolT) $ mk_bodyC vars));
     1.5                     val small_Collect = mk_CollectC (Abs("x",varsT,
     1.6                             Free ("P",varsT --> boolT) $ Bound 0));
     1.7 -                   val impl = implies $ (Mset_incl big_Collect) $ 
     1.8 -                                          (Mset_incl small_Collect);
     1.9 +                   val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    1.10     in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
    1.11  
    1.12  end;