Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified signature;
  3. clarified theory_names with exported content;
  4. proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
  5. proper treatment of empty lines (amending 08f89f0e8a62);
  6. clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
  7. merged
  8. The right way to formulate card_UNION, plus the old version for compatibility
Changeset 75863:b0215440311d by wenzelm:
merged
Changeset 75862:186654cd2840 by wenzelm:
clarified signature;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 75861:c32ecc4b4720 by wenzelm:
clarified theory_names with exported content;
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 75860:2b2c09f4e7b5 by wenzelm:
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 75859:7164f537370f by wenzelm:
proper treatment of empty lines (amending 08f89f0e8a62);
The file was modified src/Pure/library.scala (diff)
Changeset 75858:657b2de27454 by wenzelm:
clarified signature: avoid confusing operation name (amending 8cf14d4ebec4);
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/library.ML (diff)
Changeset 75857:86d60f4a10a7 by paulson:
merged
Changeset 75856:4b507edcf6b5 by paulson _lp15@cam.ac.uk_:
The right way to formulate card_UNION, plus the old version for compatibility
The file was modified src/HOL/Binomial.thy (diff)