Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. remove SpecCheck; it is now part of the AFP
  2. merged
  3. added documentation for changes to Sledgehammer option "lam_trans"
  4. jenkins: pre/post-hook results
  5. merged
  6. added opaque_combs and renamed hide_lams to opaque_lifting
Changeset 73937:fe8d0f4da0e6 by kevin kappelmann _kevin.kappelmann@tum.de_:
remove SpecCheck; it is now part of the AFP
The file was modified src/Tools/ROOT (diff)
The file was removedsrc/Tools/Spec_Check/Examples.thy
The file was removedsrc/Tools/Spec_Check/README
The file was removedsrc/Tools/Spec_Check/Spec_Check.thy
The file was removedsrc/Tools/Spec_Check/base_generator.ML
The file was removedsrc/Tools/Spec_Check/gen_construction.ML
The file was removedsrc/Tools/Spec_Check/generator.ML
The file was removedsrc/Tools/Spec_Check/output_style.ML
The file was removedsrc/Tools/Spec_Check/property.ML
The file was removedsrc/Tools/Spec_Check/random.ML
The file was removedsrc/Tools/Spec_Check/spec_check.ML
Changeset 73936:d593d18a7a92 by desharna:
merged
Changeset 73935:269b2f976100 by desharna:
added documentation for changes to Sledgehammer option "lam_trans"
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 73934:39e0c7fac69e by fabian huch _huch@in.tum.de_:
jenkins: pre/post-hook results
The file was modified src/Pure/Admin/ci_profile.scala (diff)
Changeset 73933:fa92bc604c59 by desharna:
merged
Changeset 73932:fd21b4a93043 by desharna:
added opaque_combs and renamed hide_lams to opaque_lifting
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
The file was modified src/HOL/Algebra/Coset.thy (diff)
The file was modified src/HOL/Algebra/Free_Abelian_Groups.thy (diff)
The file was modified src/HOL/Algebra/Generated_Groups.thy (diff)
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Algebra/Polynomial_Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Product_Groups.thy (diff)
The file was modified src/HOL/Algebra/Subrings.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.thy (diff)
The file was modified src/HOL/Analysis/Arcwise_Connected.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/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy (diff)
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Function_Metric.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Jordan_Curve.thy (diff)
The file was modified src/HOL/Analysis/Line_Segment.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Retracts.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Uniform_Limit.thy (diff)
The file was modified src/HOL/Auth/Message.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy (diff)
The file was modified src/HOL/Combinatorics/Cycles.thy (diff)
The file was modified src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy (diff)
The file was modified src/HOL/Complex_Analysis/Complex_Singularities.thy (diff)
The file was modified src/HOL/Complex_Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Complex_Analysis/Great_Picard.thy (diff)
The file was modified src/HOL/Complex_Analysis/Riemann_Mapping.thy (diff)
The file was modified src/HOL/Complex_Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Deriv.thy (diff)
The file was modified src/HOL/Homology/Brouwer_Degree.thy (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
The file was modified src/HOL/Homology/Simplices.thy (diff)
The file was modified src/HOL/IMP/Abs_Int2.thy (diff)
The file was modified src/HOL/IMP/Abs_Int3.thy (diff)
The file was modified src/HOL/Library/Dlist.thy (diff)
The file was modified src/HOL/Library/Equipollence.thy (diff)
The file was modified src/HOL/Library/Extended_Nonnegative_Real.thy (diff)
The file was modified src/HOL/Library/Extended_Real.thy (diff)
The file was modified src/HOL/Library/Float.thy (diff)
The file was modified src/HOL/Library/FuncSet.thy (diff)
The file was modified src/HOL/Library/Interval.thy (diff)
The file was modified src/HOL/Library/Poly_Mapping.thy (diff)
The file was modified src/HOL/Library/Word.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Nominal/Examples/Class1.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/NSA.thy (diff)
The file was modified src/HOL/Probability/Conditional_Expectation.thy (diff)
The file was modified src/HOL/Quotient_Examples/Lift_Fun.thy (diff)
The file was modified src/HOL/Real.thy (diff)
The file was modified src/HOL/Real_Vector_Spaces.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_generate.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
The file was modified src/HOL/ex/Dedekind_Real.thy (diff)