Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper Thm.trim_context;
  2. clarified stored data: actual thm allows to replay zproofs in a modular manner;
  3. tuned signature;
  4. tuned signature, following Proofterm.thm_header;
  5. more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;
  6. clarified signature;
  7. proper Thm_Name.make_list for thm_definition; tuned modules;
Changeset 79363:2c6f355e52bb by wenzelm:
proper Thm.trim_context;
The file was modified src/Pure/thm.ML (diff)
Changeset 79362:2187de552bd4 by wenzelm:
clarified stored data: actual thm allows to replay zproofs in a modular manner;
The file was modified src/Pure/thm.ML (diff)
Changeset 79361:c28d4d1986f1 by wenzelm:
tuned signature;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79360:da22c8ab0112 by wenzelm:
tuned signature, following Proofterm.thm_header;
The file was modified src/Pure/zterm.ML (diff)
Changeset 79359:5b01b93de062 by wenzelm:
more robust: avoid crash of Thm.solve_constraints due to changed background theory, e.g. relevant for AFP/Transition_Systems_and_Automata;
The file was modified src/Pure/Isar/generic_target.ML (diff)
Changeset 79358:b191339a014c by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
The file was modified src/Pure/thm_name.ML (diff)
Changeset 79357:bb07298c5fb0 by wenzelm:
proper Thm_Name.make_list for thm_definition;<br>tuned modules;
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)