made type conv pervasive;
authorwenzelm
Mon Jun 25 00:36:33 2007 +0200 (2007-06-25)
changeset 23484731658208196
parent 23483 a9356b40fbd3
child 23485 881b04972953
made type conv pervasive;
tuned;
src/HOL/Tools/Qelim/cooper.ML
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sun Jun 24 21:15:55 2007 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Jun 25 00:36:33 2007 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  signature COOPER =
     1.6   sig
     1.7 -  val cooper_conv : Proof.context -> Conv.conv
     1.8 +  val cooper_conv : Proof.context -> conv
     1.9    exception COOPER of string * exn
    1.10  end;
    1.11  
    1.12 @@ -17,9 +17,7 @@
    1.13  exception COOPER of string * exn;
    1.14  val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
    1.15  
    1.16 -fun C f x y = f y x;
    1.17 -
    1.18 -val FWD = C (fold (C implies_elim));
    1.19 +val FWD = Drule.implies_elim_list;
    1.20  
    1.21  val true_tm = @{cterm "True"};
    1.22  val false_tm = @{cterm "False"};