Hol_reln : term quotation -> thm * thm * thm
STRUCTURE
IndDefLib
SYNOPSIS
Definition facility for inductive predicates.
DESCRIBE
bossLib.Hol_reln
is identical to
IndDefLib.Hol_reln
.
SEEALSO
Hol_reln
HOL
Kananaskis-4