Skip to content
Success

Changes

Summary

  1. correction to my previous commit
  2. merged
  3. last-minute integration unscrambling
  4. towards support for HO SMT-LIB
  5. Some small lemmas about polynomials and FPSs
  6. tuned names
  7. simpler definition
  8. typo
  9. tuned
  10. tuned messages
  11. improved Vampire proof parser
  12. new file
  13. proper theory name;
  14. news
Changeset 66554:19bf4d5966dc by paulson _lp15@cam.ac.uk_:
correction to my previous commit
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
Changeset 66553:6ab32ffb2bdd by paulson:
merged
Changeset 66552:507a42c0a0ff by paulson _lp15@cam.ac.uk_:
last-minute integration unscrambling
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
Changeset 66551:4df6b0ae900d by blanchet:
towards support for HO SMT-LIB
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/Tools/SMT/cvc4_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_builtin.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_real.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_util.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_interface.ML (diff)
The file was modified src/HOL/Word/Tools/smt_word.ML (diff)
Changeset 66550:e5d82cf3c387 by eberlm _eberlm@in.tum.de_:
Some small lemmas about polynomials and FPSs
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/List.thy (diff)
Changeset 66549:b8a6f9337229 by nipkow:
tuned names
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 66548:253880668a43 by nipkow:
simpler definition
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 66547:188c7853f84a by nipkow:
typo
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 66546:14a7d2a39336 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Binomial_Heap.thy (diff)
Changeset 66545:97c441c8665d by blanchet:
tuned messages
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
Changeset 66544:3e838cf5e80c by blanchet:
improved Vampire proof parser
The file was modified src/HOL/Tools/ATP/atp_proof.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 66543:a90dbf19f573 by nipkow:
new file
The file was addedsrc/HOL/Data_Structures/Sorting.thy
The file was modified src/HOL/ROOT (diff)
Changeset 66542:075bbb78d33c by wenzelm:
proper theory name;
The file was modified NEWS (diff)
Changeset 66541:4d9c4cb9e9a5 by nipkow:
news
The file was modified NEWS (diff)