HOL.Rule
Description
rator :: Thm -> Term -> Maybe Thm Source #
ratorUnsafe :: Thm -> Term -> Thm Source #
rand :: Term -> Thm -> Maybe Thm Source #
randUnsafe :: Term -> Thm -> Thm Source #
sym :: Thm -> Maybe Thm Source #
trans :: Thm -> Thm -> Maybe Thm Source #
transUnsafe :: Thm -> Thm -> Thm Source #
proveHyp :: Thm -> Thm -> Maybe Thm Source #
alpha :: Term -> Thm -> Maybe Thm Source #
alphaHyp :: Term -> Thm -> Maybe Thm Source #
alphaSequent :: Sequent -> Thm -> Maybe Thm Source #
defineConstList :: [(Name, Var)] -> Thm -> Maybe ([Const], Thm) Source #
defineTypeOpLegacy :: Name -> Name -> Name -> [TypeVar] -> Thm -> Maybe (TypeOp, Const, Const, Thm, Thm) Source #