equal
deleted
inserted
replaced
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: |