src/HOL/Library/code_lazy.ML
changeset 70213 ff8386fc191d
parent 69597 ff784d5a5bfb
child 72154 2b41b710f6ef
equal deleted inserted replaced
70211:2388e0d2827b 70213:ff8386fc191d