src/Pure/drule.ML
changeset 22938 454f1678bf5f
parent 22906 195b7515911a
child 22939 2afc93a3d8f4
equal deleted inserted replaced
22937:08cf9aaf3aa1 22938:454f1678bf5f
    95   val compose_single: thm * int * thm -> thm
    95   val compose_single: thm * int * thm -> thm
    96   val add_rule: thm -> thm list -> thm list
    96   val add_rule: thm -> thm list -> thm list
    97   val del_rule: thm -> thm list -> thm list
    97   val del_rule: thm -> thm list -> thm list
    98   val merge_rules: thm list * thm list -> thm list
    98   val merge_rules: thm list * thm list -> thm list
    99   val imp_cong_rule: thm -> thm -> thm
    99   val imp_cong_rule: thm -> thm -> thm
       
   100   val fun_cong_rule: cterm -> thm -> thm
       
   101   val arg_cong_rule: thm -> cterm -> thm
   100   val beta_eta_conversion: cterm -> thm
   102   val beta_eta_conversion: cterm -> thm
   101   val eta_long_conversion: cterm -> thm
   103   val eta_long_conversion: cterm -> thm
   102   val eta_contraction_rule: thm -> thm
   104   val eta_contraction_rule: thm -> thm
   103   val norm_hhf_eq: thm
   105   val norm_hhf_eq: thm
   104   val is_norm_hhf: term -> bool
   106   val is_norm_hhf: term -> bool
   577         (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
   579         (implies_elim (implies_elim (assume ABC) (assume A)) (assume B)))))
   578       (implies_intr BAC (implies_intr A (implies_intr B
   580       (implies_intr BAC (implies_intr A (implies_intr B
   579         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   581         (implies_elim (implies_elim (assume BAC) (assume B)) (assume A))))))
   580   end;
   582   end;
   581 
   583 
   582 val imp_cong_rule = combination o combination (reflexive implies);
   584 val imp_cong_rule = Thm.combination o Thm.combination (Thm.reflexive implies);
       
   585 
       
   586 fun arg_cong_rule ct th = Thm.combination (Thm.reflexive ct) th;    (*AP_TERM*)
       
   587 fun fun_cong_rule th ct = Thm.combination th (Thm.reflexive ct);    (*AP_THM*)
   583 
   588 
   584 local
   589 local
   585   val dest_eq = Thm.dest_equals o cprop_of
   590   val dest_eq = Thm.dest_equals o cprop_of
   586   val rhs_of = snd o dest_eq
   591   val rhs_of = snd o dest_eq
   587 in
   592 in