Skip to content
Success

Changes

Summary

  1. merged
  2. more on product (function) topologies
  3. clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
  4. clarified error;
  5. clarified errors;
  6. suppress some theories to allow "isabelle dump -o skip_proofs";
  7. tuned signature;
Changeset 69031:30e88eabf167 by paulson:
merged
Changeset 69030:1eb517214deb by paulson _lp15@cam.ac.uk_:
more on product (function) topologies
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69029:aec64b88e708 by wenzelm:
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 69028:f440bedb8e45 by wenzelm:
clarified error;
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 69027:5ea3f424e787 by wenzelm:
clarified errors;
The file was modified src/Pure/Thy/export_theory.ML (diff)
Changeset 69026:6e2f9f62aafd by wenzelm:
suppress some theories to allow "isabelle dump -o skip_proofs";
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69025:fa7a1be0fab2 by wenzelm:
tuned signature;
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)