Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;
Changeset 70609:5549e686d6ac by wenzelm:
proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;
The file was modified src/HOL/Tools/Function/function.ML (diff)