* http://cs.unibo.it/helm/.
*)
-exception AllSelectedTermsMustBeConvertible;;
-
val assumption_tac: ProofEngineTypes.tactic
-
-val generalize_tac:
- ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
- ProofEngineTypes.lazy_pattern ->
- ProofEngineTypes.tactic
-