src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 37724 6607ccf77946
parent 36033 7106f079bd05
child 38117 5ae05823cfd9