Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper Thm.trim_context / Thm.transfer;
  2. proper position for ML-like commands;
Changeset 78036:2594319ad9ee by wenzelm:
proper Thm.trim_context / Thm.transfer;
The file was modified src/ZF/Tools/inductive_package.ML (diff)
Changeset 78035:bd5f6cee8001 by wenzelm:
proper position for ML-like commands;
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_file.ML (diff)
The file was modified src/Pure/context.ML (diff)