src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 37724 6607ccf77946
parent 36033 7106f079bd05
child 38117 5ae05823cfd9
equal deleted inserted replaced
37723:831b3eb7ed8e 37724:6607ccf77946