Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. split off theorems involving classes below metric_space and real_normed_vector
  2. merged
  3. merged
  4. tuned analysis manual
  5. tuned signature;
  6. merged
  7. clarified signature, notably cascade of dump_options, deps, resources, session;
  8. unused;
  9. clarified signature;
  10. clarified errors, according to Isabelle/MMT; tuned signature;
  11. tuned, according to Isabelle/MMT;
  12. clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;
  13. tuned;
  14. merged
  15. more capitalization
  16. capitalize proper names in lemma names
  17. explicit dependencies for includes
  18. more correct handling of symbols for includes
Changeset 69544:5aa5a8d6e5b5 by immler:
split off theorems involving classes below metric_space and real_normed_vector
The file was addedsrc/HOL/Analysis/Elementary_Metric_Spaces.thy
The file was addedsrc/HOL/Analysis/Elementary_Normed_Spaces.thy
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 69543:c2d5575d9da5 by immler:
merged
Changeset 69542:b9b7a5e2472e by immler:
merged
Changeset 69541:d466e0a639e4 by immler:
tuned analysis manual
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 69540:a1e8bcda8cec by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69539:da2726f78610 by wenzelm:
merged
Changeset 69538:faf547d2834c by wenzelm:
clarified signature, notably cascade of dump_options, deps, resources, session;
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69537:b8e8a724182b by wenzelm:
unused;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69536:892b68f932f9 by wenzelm:
clarified signature;
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 69535:e3a9680d9ed8 by wenzelm:
clarified errors, according to Isabelle/MMT;<br>tuned signature;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69534:913970ae2324 by wenzelm:
tuned, according to Isabelle/MMT;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69533:1d2e6a4e073f by wenzelm:
clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69532:e2edf24b960e by wenzelm:
tuned;
The file was modified src/Pure/Tools/dump.scala (diff)
Changeset 69531:1ae0c822682c by nipkow:
merged
Changeset 69530:fc0da2166cda by nipkow:
more capitalization
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Types_To_Sets/Examples/T2_Spaces.thy (diff)
Changeset 69529:4ab9657b3257 by nipkow:
capitalize proper names in lemma names
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Complex_Analysis_Basics.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Analysis/document/root.tex (diff)
The file was modified src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/MacLaurin.thy (diff)
The file was modified src/HOL/Probability/Probability_Mass_Function.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 69528:9d0e492e3229 by haftmann:
explicit dependencies for includes
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
The file was modified src/HOL/Library/IArray.thy (diff)
The file was modified src/HOL/Quickcheck_Narrowing.thy (diff)
Changeset 69527:3626ccf644e1 by haftmann:
more correct handling of symbols for includes
The file was modified src/Tools/Code/code_target.ML (diff)