# HG changeset patch
# User wenzelm
# Date 1295193709 -3600
# Node ID 6eeda4b417b31b931ad2950aa89b56347239cc62
# Parent  bbd861837ebc01b29283130e5605961f4beb7c54
non-executable sources;

diff -r bbd861837ebc -r 6eeda4b417b3 src/Tools/interpretation_with_defs.ML