src/HOL/Transitive_Closure.ML
changeset 15485 e93a3badc2bc
parent 13704 854501b1e957