src/HOL/Extraction/ROOT.ML
changeset 30082 43c5b7bfc791
parent 25420 0fe95159787a
child 32479 521cc9bf2958
equal deleted inserted replaced
30081:46b9c8ae3897 30082:43c5b7bfc791