Skip to content
Success

Changes

Summary

  1. clarified -- avoid non-standard extend/merge;
  2. tuned -- avoid non-standard extend;
  3. clarified -- avoid non-standard extend/merge;
  4. proper session imports;
  5. clarified -- avoid non-standard extend;
  6. tuned -- avoid non-standard extend/merge;
  7. prefer conservative extend/merge of theory naming;
Changeset 72059:69880fdc8310 by wenzelm:
clarified -- avoid non-standard extend/merge;
The file was modified src/Pure/theory.ML (diff)
Changeset 72058:f8d28617ea08 by wenzelm:
tuned -- avoid non-standard extend;
The file was modified src/Pure/sign.ML (diff)
Changeset 72057:ce3f26b4e790 by wenzelm:
clarified -- avoid non-standard extend/merge;
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 72056:b9f5f30b623f by wenzelm:
proper session imports;
The file was modified src/HOL/ROOT (diff)
Changeset 72055:deb390860f07 by wenzelm:
clarified -- avoid non-standard extend;
The file was modified src/Pure/global_theory.ML (diff)
Changeset 72054:6c75287276d5 by wenzelm:
tuned -- avoid non-standard extend/merge;
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 72053:4ed33ea8d957 by wenzelm:
prefer conservative extend/merge of theory naming;
The file was modified src/Pure/General/name_space.ML (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/Pure/sign.ML (diff)
The file was modified src/Pure/theory.ML (diff)