src/HOL/Tools/function_package/context_tree.ML
changeset 27249 f339dc43ce9f
parent 26529 03ad378ed5f0
child 27330 1af2598b5f7d
equal deleted inserted replaced
27248:3c17b824650b 27249:f339dc43ce9f