src/HOL/IMP/ROOT.ML
changeset 26462 dac4e2bce00d
parent 24104 719fbe4fb77f
child 28583 9bb9791bdc18