Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. prefer persistent hash code for cachable items (see also 72b13af7f266);
  2. merged
  3. more operations: record overall exported entities;
  4. merged
  5. added dummy_fof prover to Sledgehammer
  6. fixed malconfigured option output_dir in mirabelle
  7. merged
  8. clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
  9. proper name space "kind": this is a formal name, not comment;
  10. more uniform signatures in ML and Scala;
  11. merged
  12. fixed typo
  13. added dummy_thf prover to Sledgehammer
Changeset 74121:bc03b0b82fe6 by wenzelm:
prefer persistent hash code for cachable items (see also 72b13af7f266);
The file was modified src/Pure/term.scala (diff)
Changeset 74120:21ddf56ac140 by wenzelm:
merged
Changeset 74119:342d0298e164 by wenzelm:
more operations: record overall exported entities;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 74118:49884e54f13a by desharna:
merged
Changeset 74117:30ab39ab4117 by desharna:
added dummy_fof prover to Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
Changeset 74116:5cd8b5cd0451 by desharna:
fixed malconfigured option output_dir in mirabelle
The file was modified src/HOL/Tools/Mirabelle/mirabelle.scala (diff)
Changeset 74115:8752420f3377 by wenzelm:
merged
Changeset 74114:700e5bd59c7d by wenzelm:
clarified export of formal entities: name space info is always present, but content depends on option "export_theory";
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/typedef.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 74113:228adc502803 by wenzelm:
proper name space "kind": this is a formal name, not comment;
The file was modified src/HOL/Real_Asymp/exp_log_expression.ML (diff)
The file was modified src/HOL/Real_Asymp/multiseries_expansion.ML (diff)
Changeset 74112:d0527bb2e590 by wenzelm:
more uniform signatures in ML and Scala;
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/facts.ML (diff)
The file was modified src/Pure/theory.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 74111:58e208ad4bcf by desharna:
merged
Changeset 74110:6c7feeef0ff2 by desharna:
fixed typo
The file was modified NEWS (diff)
Changeset 74109:ed1f576df9c4 by desharna:
added dummy_thf prover to Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)