Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
  2. add lemmas about prod_filter
  3. merged
  4. corrections to markup
  5. updated material concerning Algebra
  6. merged
  7. de-applying
  8. added system option "strict_facts";
Changeset 68668:c9570658e8f1 by blanchet:
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
Changeset 68667:96aae7c44bb2 by Andreas Lochbihler:
add lemmas about prod_filter
The file was modified src/HOL/Filter.thy (diff)
Changeset 68666:4bee4828cfc3 by paulson:
merged
Changeset 68665:94b08469980e by paulson _lp15@cam.ac.uk_:
corrections to markup
The file was modified src/HOL/Algebra/Ring_Divisibility.thy (diff)
Changeset 68664:bd0df72c16d5 by paulson _lp15@cam.ac.uk_:
updated material concerning Algebra
The file was modified src/HOL/Algebra/Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Generated_Rings.thy (diff)
The file was modified src/HOL/Algebra/Polynomials.thy (diff)
The file was modified src/HOL/Algebra/RingHom.thy (diff)
The file was modified src/HOL/Algebra/Ring_Divisibility.thy (diff)
The file was modified src/HOL/Algebra/Subrings.thy (diff)
Changeset 68663:00a872706648 by paulson:
merged
Changeset 68662:227f85b1b98c by paulson _lp15@cam.ac.uk_:
de-applying
The file was modified src/HOL/Algebra/Group.thy (diff)
The file was modified src/HOL/Real.thy (diff)
Changeset 68661:5820f0f379ae by wenzelm:
added system option "strict_facts";
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/global_theory.ML (diff)