Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. NEWS;
  2. merged
  3. export thm_deps;
  4. proper theory context;
  5. clarified thm_id vs. thm_node/thm: retain theory_name; support for thm_deps: expand unnamed nodes;
  6. clarified signature;
  7. tuned;
  8. unused (see 095dadc62bb5);
  9. tuned;
  10. tuned signature;
  11. clarified modules;
  12. clarified modules;
  13. tuned;
  14. clarified signature;
  15. tuned
  16. tuned
  17. merged
  18. tuned
Changeset 70599:853947643971 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 70598:a56b4e59bfd1 by wenzelm:
merged
Changeset 70597:a896257a3f07 by wenzelm:
export thm_deps;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 70596:3a7117c33742 by wenzelm:
proper theory context;
The file was modified src/Pure/Thy/thm_deps.ML (diff)
Changeset 70595:2ae7e33c950f by wenzelm:
clarified thm_id vs. thm_node/thm: retain theory_name;<br>support for thm_deps: expand unnamed nodes;
The file was modified src/Pure/Thy/thm_deps.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70594:64b5514c33b1 by wenzelm:
clarified signature;
The file was modified src/Pure/global_theory.ML (diff)
Changeset 70593:1d239ebba0e3 by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70592:78426ea26f12 by wenzelm:
unused (see 095dadc62bb5);
The file was modified src/Pure/thm.ML (diff)
Changeset 70591:38cc9b2c5a94 by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70590:8214aa5d5650 by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70589:00b67aaa4010 by wenzelm:
clarified modules;
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70588:35a4ef9c6d80 by wenzelm:
clarified modules;
The file was modified src/Pure/Thy/thm_deps.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70587:729f4d066d1a by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 70586:57df8a85317a by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_redirect.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_nut.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/Pure/General/heap.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
The file was modified src/Pure/General/table.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/Syntax/lexicon.ML (diff)
The file was modified src/Pure/context.ML (diff)
The file was modified src/Pure/defs.ML (diff)
The file was modified src/Pure/library.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/thm_name.ML (diff)
The file was modified src/Pure/variable.ML (diff)
The file was modified src/Tools/Argo/argo_expr.ML (diff)
The file was modified src/Tools/Argo/argo_proof.ML (diff)
The file was modified src/Tools/Argo/argo_term.ML (diff)
The file was modified src/Tools/float.ML (diff)
Changeset 70585:eecade21bc6a by nipkow:
tuned
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
The file was modified src/HOL/Data_Structures/Leftist_Heap.thy (diff)
Changeset 70584:f7c1f585edeb by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Set2_Join_RBT.thy (diff)
The file was modified src/HOL/Data_Structures/Set_Specs.thy (diff)
Changeset 70583:17909568216e by nipkow:
merged
Changeset 70582:7beee08eb163 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Set2_Join.thy (diff)
The file was modified src/HOL/Data_Structures/Set2_Join_RBT.thy (diff)