src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 36832 e6078ef937df
parent 36033 7106f079bd05
child 38117 5ae05823cfd9