src/HOL/Tools/function_package/context_tree.ML
changeset 24403 b7c3ee2ca184
parent 24168 86a03a092062
child 24977 9f98751c9628