src/HOL/Library/code_lazy.ML
changeset 80321 31b9dfbe534c
parent 74561 8e6c973003c8
child 80634 a90ab1ea6458
equal deleted inserted replaced
80318:cdf26ac90f87 80321:31b9dfbe534c