src/HOL/Extraction/ROOT.ML
changeset 33604 d4220df6fde2
parent 32479 521cc9bf2958
child 34205 f69cd974bc4e