src/Pure/drule.ML
changeset 23568 afecdba16452
parent 23537 ecf487dce798
child 24005 2d473ed15491
--- 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