src/HOL/Hoare_Parallel/ROOT.ML

fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies

use_thys ["Hoare_Parallel"];