Documentation
Aesop
.
RuleTac
.
Forward
Search
return to top
source
Imports
Init
Aesop.Forward.Match
Aesop.RuleTac.Basic
Aesop.RuleTac.ElabRuleTerm
Aesop.Script.SpecificTactics
Aesop.RuleTac.Forward.Basic
Batteries.Lean.Meta.UnusedNames
Imported by