src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 38958 08eb0ffa2413
parent 38948 c4e6afaa8dcd
child 39184 71f3f194b962