HOL-ex.Transitive_Closure_Table_Ex