Summary
- clarified -- avoid non-standard extend/merge;
- tuned -- avoid non-standard extend;
- clarified -- avoid non-standard extend/merge;
- proper session imports;
- clarified -- avoid non-standard extend;
- tuned -- avoid non-standard extend/merge;
- prefer conservative extend/merge of theory naming;
The file was modified | src/Pure/theory.ML (diff) |
The file was modified | src/Pure/sign.ML (diff) |
The file was modified | src/Pure/Isar/code.ML (diff) |
The file was modified | src/Tools/Code/code_target.ML (diff) |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/Pure/global_theory.ML (diff) |
The file was modified | src/Pure/ML/ml_thms.ML (diff) |
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) |