Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified signature;
  3. clarified export of axioms and theorems (identified derivations instead of projected facts);
  4. tuned signature;
  5. back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
  6. module Thm_Name for Isabelle/Scala;
  7. tuned;
  8. clarified modules;
  9. tuned;
  10. tuned
  11. tuned names
Changeset 70581:ea860617fac1 by wenzelm:
merged
Changeset 70580:e6101f131d0d by wenzelm:
clarified signature;
The file was modified src/Pure/thm_name.scala (diff)
Changeset 70579:5a8e3e4b3760 by wenzelm:
clarified export of axioms and theorems (identified derivations instead of projected facts);
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 70578:7bb2bbb3ccd6 by wenzelm:
tuned signature;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70577:ed651a58afe4 by wenzelm:
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70576:3554531505a8 by wenzelm:
module Thm_Name for Isabelle/Scala;
The file was addedsrc/Pure/thm_name.scala
The file was modified src/Pure/build-jars (diff)
Changeset 70575:bf1a59014481 by wenzelm:
tuned;
The file was modified src/Pure/thm_name.ML (diff)
Changeset 70574:503ca64329cc by wenzelm:
clarified modules;
The file was addedsrc/Pure/thm_name.ML
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/facts.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)
Changeset 70573:10dd61d9357a by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 70572:b63e5e4598d7 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Set2_Join.thy (diff)
Changeset 70571:e72daea2aab6 by nipkow:
tuned names
The file was modified src/HOL/Data_Structures/AVL_Set.thy (diff)
The file was modified src/HOL/Data_Structures/RBT.thy (diff)
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)