src/Pure/conv.ML
changeset 41248 bb28bf635202
parent 38668 e8236c4aff16
child 42485 4faf82d12b19
equal deleted inserted replaced
41247:c5cb19ecbd41 41248:bb28bf635202
    46   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    46   val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
    47   val prems_conv: int -> conv -> conv
    47   val prems_conv: int -> conv -> conv
    48   val concl_conv: int -> conv -> conv
    48   val concl_conv: int -> conv -> conv
    49   val fconv_rule: conv -> thm -> thm
    49   val fconv_rule: conv -> thm -> thm
    50   val gconv_rule: conv -> int -> thm -> thm
    50   val gconv_rule: conv -> int -> thm -> thm
    51   val tap_thy: (theory -> conv) -> conv
       
    52 end;
    51 end;
    53 
    52 
    54 structure Conv: CONV =
    53 structure Conv: CONV =
    55 struct
    54 struct
    56 
    55 
   210         if Thm.is_reflexive eq then th
   209         if Thm.is_reflexive eq then th
   211         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   210         else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th
   212       end
   211       end
   213   | NONE => raise THM ("gconv_rule", i, [th]));
   212   | NONE => raise THM ("gconv_rule", i, [th]));
   214 
   213 
   215 
       
   216 fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
       
   217 
       
   218 end;
   214 end;
   219 
   215 
   220 structure Basic_Conv: BASIC_CONV = Conv;
   216 structure Basic_Conv: BASIC_CONV = Conv;
   221 open Basic_Conv;
   217 open Basic_Conv;