src/HOL/Tools/function_package/context_tree.ML
changeset 27018 b3e63f39fc0f
parent 26529 03ad378ed5f0
child 27330 1af2598b5f7d
equal deleted inserted replaced
27017:1e0e8c1adf8c 27018:b3e63f39fc0f