| Source File | Identifier index | Theory binding index |
|---|
signature resolve_then = sig include Abbrev datatype match_position = datatype thmpos_dtype.match_position val resolve_then : match_position -> thm_tactic -> thm -> thm -> tactic end
| Source File | Identifier index | Theory binding index |
|---|