Skip to content
Failed

Changes

Summary

  1. moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
  2. tuned;
  3. removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML);
  4. clarified signature;
  5. clarified modules: more official Sessions.notable_groups;
  6. tuned
  7. merged
  8. An assortment of new material, mostly due to Manuel
Changeset 80785:f9e38496cf57 by manuel eberl _eberlm@in.tum.de_:
moved over material from AFP; most importantly on algebraic numbers and algebraically closed fields
The file was addedsrc/HOL/Computational_Algebra/document/root.bib
The file was addedsrc/HOL/Computational_Algebra/document/root.tex
The file was modified src/HOL/Computational_Algebra/Formal_Laurent_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Fraction_Field.thy (diff)
The file was modified src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Groups_List.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
The file was modified src/HOL/Library/Real_Mod.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Rat.thy (diff)
The file was modified src/Pure/General/toml.scala (diff)
Changeset 80783:87f90735e6dd by wenzelm:
removed unused/obsolete material: some of it was motivated by Isabelle/MMT (e.g. f150253cb201), but is superseded by AFP metadata (TOML);
The file was modified src/Pure/Admin/afp.scala (diff)
Changeset 80782:9279e96eb34e by wenzelm:
clarified signature;
The file was modified src/Pure/Admin/afp.scala (diff)
The file was modified src/Pure/Build/build.scala (diff)
The file was modified src/Pure/Build/build_schedule.scala (diff)
Changeset 80781:42bc8ab751c1 by wenzelm:
clarified modules: more official Sessions.notable_groups;
The file was modified src/Pure/Admin/afp.scala (diff)
The file was modified src/Pure/Admin/build_status.scala (diff)
The file was modified src/Pure/Build/sessions.scala (diff)
Changeset 80780:f8d7df38d7c6 by nipkow:
tuned
The file was modified src/Doc/Prog_Prove/Isar.thy (diff)
Changeset 80779:44d8fb3da9d5 by paulson:
merged
Changeset 80778:35b2143aeec6 by paulson _lp15@cam.ac.uk_:
An assortment of new material, mostly due to Manuel
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Smooth_Paths.thy (diff)
The file was modified src/HOL/Complex_Analysis/Contour_Integration.thy (diff)
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)