Summary
- merged
- more on product (function) topologies
- clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
- clarified error;
- clarified errors;
- suppress some theories to allow "isabelle dump -o skip_proofs";
- tuned signature;
The file was modified | src/HOL/Analysis/Function_Topology.thy (diff) |
The file was modified | src/HOL/Analysis/Topology_Euclidean_Space.thy (diff) |
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.ML (diff) |
The file was modified | src/Pure/Thy/export_theory.ML (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Tools/dump.scala (diff) |
The file was modified | src/Pure/Thy/sessions.scala (diff) |
The file was modified | src/Pure/Tools/dump.scala (diff) |