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