Theory ML_Unification.ML_Term_Index

✐‹creator "Kevin Kappelmann"›
section ‹Term Indexing›
theory ML_Term_Index
  imports
    ML_Normalisations
begin

paragraph ‹Summary›
text ‹Termin indexes signatures and implementations.›

ML_file‹term_index.ML›
ML_file‹discrimination_tree.ML›

ML_file‹term_index_data.ML›

end