1\DOC Hol_reln
2
3\TYPE {Hol_reln : term quotation -> thm * thm * thm}
4
5\SYNOPSIS
6Definition facility for inductive predicates.
7
8\DESCRIBE
9{bossLib.Hol_reln} is identical to {IndDefLib.Hol_reln}.
10
11\SEEALSO
12bossLib.Hol_reln.
13
14\ENDDOC
15