[isabelle] transitive closure
trancl :: "('a × 'a) set => ('a × 'a) set" ("(_^+)"  999)
for r :: "('a × 'a) set"
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
| trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==>
(b, c) : r ==> (a, c) : r^+"
but this doesn't seem to work right with new style relations, e.g.
term "(less :: nat => nat => bool)^+"
produces a type error. Is there a transitive closure operator for new
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and