src/HOL/Predicate_Compile_Examples/ROOT.ML
changeset 40847 df8c7dc30214
parent 40243 3102b27ca03a
child 41952 c7297638599b
equal deleted inserted replaced
40846:5a2ae8cc9d0e 40847:df8c7dc30214