Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
  2. bundle syntax for inner
  3. merged
  4. tuned;
  5. support pruning of export names;
  6. clarified signature;
  7. Reorg of material
  8. redundant lemma
  9. tuned headers
  10. Reorg of material
  11. tuned headers
  12. merged
  13. moved and renamed class
Changeset 69675:880ab0f27ddf by immler:
Reorg, in particular Determinants as well as some linear algebra from Starlike and Change_Of_Vars
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Convex.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
Changeset 69674:fc252acb7100 by immler:
bundle syntax for inner
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
Changeset 69673:cc47e7e06f38 by wenzelm:
merged
Changeset 69672:f97fbb2330aa by wenzelm:
tuned;
The file was modified NEWS (diff)
Changeset 69671:2486792eaf61 by wenzelm:
support pruning of export names;
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/sessions.ML (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 69670:114ae60c4be7 by wenzelm:
clarified signature;
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
Changeset 69669:de2f0a24b0f0 by nipkow:
Reorg of material
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
Changeset 69668:14a8cac10eac by nipkow:
redundant lemma
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
Changeset 69667:82bb6225588b by nipkow:
tuned headers
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
Changeset 69666:d51e5e41fafe by nipkow:
Reorg of material
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
Changeset 69665:60110f6d0b4e by nipkow:
tuned headers
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
Changeset 69664:839ebe61786f by nipkow:
merged
Changeset 69663:41ff40bf1530 by nipkow:
moved and renamed class
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)