src/FOL/hypsubstdata.ML
changeset 12345 5d1436d1c268
parent 9528 95852b4be214
child 12353 e4be26df707a
equal deleted inserted replaced
12344:7237c6497cb1 12345:5d1436d1c268
    17 		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    17 		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    18   end;
    18   end;
    19 
    19 
    20 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    20 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    21 open Hypsubst;
    21 open Hypsubst;
       
    22 
       
    23 fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
       
    24   Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("o", []) | _ => false)
       
    25     (Library.nth_elem (i - 1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm;