Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. updated news
  2. get rid of visibility in MaSh -- it slows it down more than it helps
  3. merged
  4. updated polyml platform: 32=x86_64_32;
  5. more thorough purge_platforms;
  6. clarified ML_OPTIONS on Windows;
  7. more operations;
  8. new material about summations and powers, along with some tweaks
  9. dedicated combinator for declarations nested in a local theory block
  10. more conventional parsing of code_stmts antiquotation
  11. more conventional syntax for code_stmts antiquotation
Changeset 69707:920fe0a2fd22 by blanchet:
updated news
The file was modified NEWS (diff)
Changeset 69706:6d6235b828fc by blanchet:
get rid of visibility in MaSh -- it slows it down more than it helps
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
Changeset 69705:c9ea1e9916fb by wenzelm:
merged
Changeset 69704:3fb94d9b87b0 by wenzelm:
updated polyml platform: 32=x86_64_32;
The file was modified Admin/polyml/README (diff)
The file was modified Admin/polyml/settings (diff)
The file was modified src/Pure/Admin/build_polyml.scala (diff)
Changeset 69703:1e30b4093924 by wenzelm:
more thorough purge_platforms;
The file was modified src/Pure/Admin/components.scala (diff)
Changeset 69702:1adc89c4a795 by wenzelm:
clarified ML_OPTIONS on Windows;
The file was modified src/Pure/ML/ml_process.scala (diff)
Changeset 69701:b5ecabcfb780 by wenzelm:
more operations;
The file was modified src/Pure/ML/ml_system.ML (diff)
Changeset 69700:7a92cbec7030 by paulson _lp15@cam.ac.uk_:
new material about summations and powers, along with some tweaks
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Lattice.thy (diff)
The file was modified src/HOL/Algebra/Weak_Morphisms.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Embed_Measure.thy (diff)
The file was modified src/HOL/Fun.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Int.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Finite_Map.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/StarDef.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/Set.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
Changeset 69699:82f57315cade by haftmann:
dedicated combinator for declarations nested in a local theory block
The file was modified src/Pure/Isar/interpretation.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
Changeset 69698:1a249d1c884b by haftmann:
more conventional parsing of code_stmts antiquotation
The file was modified src/Tools/Code/code_target.ML (diff)
Changeset 69697:4d95261fab5a by haftmann:
more conventional syntax for code_stmts antiquotation
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Foundations.thy (diff)
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/Doc/Codegen/Refinement.thy (diff)
The file was modified src/Tools/Code/code_target.ML (diff)