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