src/HOL/Library/code_lazy.ML
changeset 78893 3645442be6d5
parent 74561 8e6c973003c8
child 80634 a90ab1ea6458
equal deleted inserted replaced
78892:aaf2cf463e9a 78893:3645442be6d5