Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
  2. clarified signature: proper typargs;
  3. merged
  4. export locale content; read_theory_names: proper classrel, arities; tuned signature;
  5. tuned;
Changeset 68865:dd44e31ca2c6 by wenzelm:
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
Changeset 68864:1dacce27bc25 by wenzelm:
clarified signature: proper typargs;
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 68863:a0769c7f51b4 by wenzelm:
merged
Changeset 68862:47e9912c53c3 by wenzelm:
export locale content;<br>read_theory_names: proper classrel, arities;<br>tuned signature;
The file was modified src/Pure/Isar/locale.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 68861:2d99562a7fe2 by wenzelm:
tuned;
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)