changeset 9108 | 9fff97d29837 |
parent 8703 | 816d8f6513be |
child 9181 | 25f993973fac |
--- a/src/HOL/WF.ML Thu Jun 22 11:37:13 2000 +0200 +++ b/src/HOL/WF.ML Thu Jun 22 23:04:34 2000 +0200 @@ -68,6 +68,8 @@ "!!X. wf (r^-1) ==> wf ((r^+)^-1)" (K [ stac (trancl_converse RS sym) 1, etac wf_trancl 1]); +bind_thm ("wf_converse_trancl", wf_converse_trancl); + (*---------------------------------------------------------------------------- * Minimal-element characterization of well-foundedness