Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. merged
  2. an assortment of new or stronger lemmas
  3. obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
  4. print outcome of Sledgehammer search in panel
  5. print Sledgehammer error message
Changeset 75079:8a48a9be91ce by paulson:
merged
Changeset 75078:ec86cb2418e1 by paulson _lp15@cam.ac.uk_:
an assortment of new or stronger lemmas
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy
The file was modified src/HOL/Analysis/Continuum_Not_Denumerable.thy
The file was modified src/HOL/Analysis/Derivative.thy
The file was modified src/HOL/Analysis/Lebesgue_Measure.thy
The file was modified src/HOL/Groups_Big.thy
The file was modified src/HOL/Library/FuncSet.thy
Changeset 75077:32947e5c453d by wenzelm:
obsolete (reverting b3d6bb2ebf77): Isabelle/Naproche cache is now value-oriented;
The file was modified src/Pure/Isar/toplevel.ML
Changeset 75076:3bcbc4d12916 by blanchet:
print outcome of Sledgehammer search in panel
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML
Changeset 75075:27c93bfb0016 by blanchet:
print Sledgehammer error message
The file was modified src/HOL/Tools/ATP/atp_proof.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML

Summary

  1. merged
  2. More material
  3. added idempotent most general unifier
  4. used same parameter order for locales substitution and substitution
  5. patched for new/simplified lemmas
  6. Better notation.
Changeset 12422:390f230578c5 by nipkow:
merged
Changeset 12421:78b756217908 by nipkow:
More material
The file was modified thys/Weight_Balanced_Trees/Weight_Balanced_Trees_log.thy
Changeset 12420:f6456079a297 by desharna:
added idempotent most general unifier
The file was modified thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
The file was modified thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
Changeset 12419:529f5f3d2da0 by desharna:
used same parameter order for locales substitution and substitution
The file was modified thys/Functional_Ordered_Resolution_Prover/IsaFoR_Term.thy
The file was modified thys/Ordered_Resolution_Prover/Abstract_Substitution.thy
The file was modified thys/Ordered_Resolution_Prover/FO_Ordered_Resolution.thy
Changeset 12418:f7df1a1ea10c by paulson _lp15@cam.ac.uk_:
patched for new/simplified lemmas
The file was modified thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy
The file was modified thys/Sunflowers/Erdos_Rado_Sunflower.thy
Changeset 12417:b74da009ae6d by asta halkjær from _andro.from@gmail.com_:
Better notation.
The file was modified thys/Epistemic_Logic/Epistemic_Logic.thy
The file was modified thys/Public_Announcement_Logic/PAL.thy