src/HOL/Tools/function_package/context_tree.ML
changeset 24434 c588ec4cf194
parent 24168 86a03a092062
child 24977 9f98751c9628
equal deleted inserted replaced
24433:4a405457e9d6 24434:c588ec4cf194