added fun/arg_cong_rule;
authorwenzelm
Fri May 11 18:47:08 2007 +0200 (2007-05-11)
changeset 22938454f1678bf5f
parent 22937 08cf9aaf3aa1
child 22939 2afc93a3d8f4
added fun/arg_cong_rule;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri May 11 18:46:50 2007 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri May 11 18:47:08 2007 +0200
     1.3 @@ -97,6 +97,8 @@
     1.4    val del_rule: thm -> thm list -> thm list
     1.5    val merge_rules: thm list * thm list -> thm list
     1.6    val imp_cong_rule: thm -> thm -> thm
     1.7 +  val fun_cong_rule: cterm -> thm -> thm
     1.8 +  val arg_cong_rule: thm -> cterm -> thm
     1.9    val beta_eta_conversion: cterm -> thm
    1.10    val eta_long_conversion: cterm -> thm
    1.11    val eta_contraction_rule: thm -> thm
    1.12 @@ -579,7 +581,10 @@
    1.13          (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
    1.14    end;
    1.15  
    1.16 -val imp_cong_rule = combination o combination (reflexive implies);
    1.17 +val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
    1.18 +
    1.19 +fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM*)
    1.20 +fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM*)
    1.21  
    1.22  local
    1.23    val dest_eq = Thm.dest_equals o cprop_of