src/HOL/Tools/function_package/context_tree.ML
changeset 23975 06f52a99fbd2
parent 23819 2040846d1bbe
child 24168 86a03a092062
equal deleted inserted replaced
23974:16ecf0a5a6bb 23975:06f52a99fbd2