src/Provers/hypsubst.ML
changeset 42799 4e33894aec6d
parent 42366 2305c70ec9b1
child 43333 2bdec7f430d3
equal deleted inserted replaced
42798:02c88bdabe75 42799:4e33894aec6d
    51   val blast_hyp_subst_tac    : bool -> int -> tactic
    51   val blast_hyp_subst_tac    : bool -> int -> tactic
    52   val stac                   : thm -> int -> tactic
    52   val stac                   : thm -> int -> tactic
    53   val hypsubst_setup         : theory -> theory
    53   val hypsubst_setup         : theory -> theory
    54 end;
    54 end;
    55 
    55 
    56 functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
    56 functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
    57 struct
    57 struct
    58 
    58 
    59 exception EQ_VAR;
    59 exception EQ_VAR;
    60 
    60 
    61 (*Simplifier turns Bound variables to special Free variables:
    61 (*Simplifier turns Bound variables to special Free variables: