# HG changeset patch
# User wenzelm
# Date 1183560576 -7200
# Node ID afecdba1645276c7597960ca33807cb4cb00611c
# Parent  28c6a0118818dfc346a9812665fa3971c230b771
added binop_cong_rule;

diff -r 28c6a0118818 -r afecdba16452 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jul 04 16:49:35 2007 +0200
+++ b/src/Pure/drule.ML	Wed Jul 04 16:49:36 2007 +0200
@@ -98,6 +98,7 @@
   val merge_rules: thm list * thm list -> thm list
   val imp_cong_rule: thm -> thm -> thm
   val arg_cong_rule: cterm -> thm -> thm
+  val binop_cong_rule: cterm -> thm -> thm -> thm
   val fun_cong_rule: thm -> cterm -> thm
   val beta_eta_conversion: cterm -> thm
   val eta_long_conversion: cterm -> thm
@@ -589,6 +590,7 @@
 
 fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM in LCF/HOL*)
 fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM in LCF/HOL*)
+fun binop_cong_rule ct th1 th2 = Thm.combination (arg_cong_rule ct th1) th2;
 
 local
   val dest_eq = Thm.dest_equals o cprop_of