Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper Thm.trim_context / Thm.transfer;
  2. proper Thm.trim_context / Thm.transfer;
  3. tuned;
  4. tuned Isabelle/ML;
  5. more informative position information;
  6. tuned;
  7. more informative position information;
  8. clarified context tracing; proper finish: purge inactive entries;
  9. more operations;
  10. proper system options to control context tracing/timing;
  11. added lemmas transp_on_multpHO and transp_multpHO
  12. tuned theory structure
  13. merged
  14. added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
Changeset 78027:4bb7eb16b867 by wenzelm:
proper Thm.trim_context / Thm.transfer;
The file was modified src/HOL/Tools/Lifting/lifting_info.ML (diff)
Changeset 78026:af3f1a4ba6e4 by wenzelm:
proper Thm.trim_context / Thm.transfer;
The file was modified src/HOL/Tools/SMT/z3_replay_rules.ML (diff)
Changeset 78025:51d135645d70 by wenzelm:
tuned;
The file was modified src/HOL/Tools/SMT/z3_replay_rules.ML (diff)
Changeset 78024:261b527f1b03 by wenzelm:
tuned Isabelle/ML;
The file was modified src/HOL/Tools/Lifting/lifting_info.ML (diff)
Changeset 78023:76dece8cd8a7 by wenzelm:
more informative position information;
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
Changeset 78022:c078a33c2dff by wenzelm:
tuned;
The file was modified src/ZF/Tools/induct_tacs.ML (diff)
Changeset 78021:ce6e3bc34343 by wenzelm:
more informative position information;
The file was modified src/Pure/Concurrent/thread_position.ML (diff)
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/General/position.scala (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Tools/Haskell/Haskell.thy (diff)
Changeset 78020:1a829342a2d3 by wenzelm:
clarified context tracing;<br>proper finish: purge inactive entries;
The file was modified src/Pure/PIDE/session.ML (diff)
The file was modified src/Pure/context.ML (diff)
Changeset 78019:82b09fd28504 by wenzelm:
more operations;
The file was modified src/Pure/Concurrent/unsynchronized.ML (diff)
Changeset 78018:dfa44d85d751 by wenzelm:
proper system options to control context tracing/timing;
The file was modified etc/options (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/context.ML (diff)
Changeset 78017:db041670d6bb by desharna:
added lemmas transp_on_multpHO and transp_multpHO
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
Changeset 78016:b0ef3aae2bdb by desharna:
tuned theory structure
The file was modified src/HOL/Library/Multiset_Order.thy (diff)
Changeset 78015:93f294ad42e6 by desharna:
merged
Changeset 78014:24f0cd70790b by desharna:
added lemmas Finite_Set.bex_(min|max)_element_with_property and reordered assumptions of Finite_Set.bex_(min|max)_element
The file was modified NEWS (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/Multiset_Order.thy (diff)