Skip to content
Success

Changes

Summary

  1. tagged 8 theories for the Analysis manual.
  2. merged
  3. more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
  4. more portable tar_options;
  5. check (non-)executable files -- and eliminate them manually from the repository)
  6. eliminated "isabelle makedist" -- prefer Scala over bash/perl scripting; eliminated "isabelle news"; roper title in NEWS.html; more robust build of documentation, using proper Other_Isabelle settings: avoid conflict with enclosing ISABELLE_OCAML / ISABELLE_GHC; misc tuning and clarification;
  7. tuned signature;
  8. tuned signature;
  9. updated PLATFORMS;
  10. uniform naming of strong congruence rules
  11. added lemma
Changeset 69173:38beaaebe736 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
tagged 8 theories for the Analysis manual.
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Radon_Nikodym.thy (diff)
The file was modified src/HOL/Analysis/Regularity.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Analysis/Simplex_Content.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
Changeset 69172:55a9803cb6be by wenzelm:
merged
Changeset 69171:710845a85944 by wenzelm:
more robust release.read_ident: eliminated odd state files ISABELLE_IDENT, ISABELLE_DIST;
The file was modified src/Pure/Admin/build_release.scala (diff)
Changeset 69170:6d28536481ad by wenzelm:
more portable tar_options;
The file was modified src/Pure/Admin/build_release.scala (diff)
Changeset 69169:a5640ec8fcb8 by wenzelm:
check (non-)executable files -- and eliminate them manually from the repository)
The file was modified Admin/Release/CHECKLIST (diff)
The file was modified src/Pure/Admin/build_release.scala (diff)
Changeset 69168:68816d1c73a7 by wenzelm:
eliminated &quot;isabelle makedist&quot; -- prefer Scala over bash/perl scripting;<br>eliminated &quot;isabelle news&quot;;<br>roper title in NEWS.html;<br>more robust build of documentation, using proper Other_Isabelle settings: avoid conflict with enclosing ISABELLE_OCAML / ISABELLE_GHC;<br>misc tuning and clarification;
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/Admin/other_isabelle.scala (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
The file was modified src/Pure/System/isabelle_tool.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was removedAdmin/lib/Tools/makedist
The file was removedsrc/Pure/Admin/news.scala
Changeset 69167:9456ba573729 by wenzelm:
tuned signature;
The file was modified src/Pure/Admin/build_release.scala (diff)
Changeset 69166:5c553c48c0e5 by wenzelm:
tuned signature;
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Pure/Admin/other_isabelle.scala (diff)
Changeset 69165:c360f3b603f8 by wenzelm:
updated PLATFORMS;
The file was modified Admin/PLATFORMS (diff)
Changeset 69164:74f1b0f10b2b by nipkow:
uniform naming of strong congruence rules
The file was modified NEWS (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Hoare_Parallel/OG_Examples.thy (diff)
The file was modified src/HOL/Hoare_Parallel/RG_Examples.thy (diff)
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Groups_Big_Fun.thy (diff)
The file was modified src/HOL/Number_Theory/Gauss.thy (diff)
The file was modified src/HOL/Probability/Information.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
Changeset 69163:6c9453ec2191 by nipkow:
added lemma
The file was modified src/HOL/Set.thy (diff)