Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned: more standard use of order;
  2. tuned;
  3. tuned;
  4. clarified signature; eliminated aliases of Thm.term_ord;
  5. clarified signature: prefer proper order operation;
  6. tuned signature: more operations;
  7. clarified signature;
Changeset 67565:e13378b304dd by wenzelm:
tuned: more standard use of order;
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
Changeset 67564:d615e9ca77dc by wenzelm:
tuned;
The file was modified src/HOL/Library/positivstellensatz.ML (diff)
Changeset 67563:6e5316a43079 by wenzelm:
tuned;
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
Changeset 67562:2427d3e72b6e by wenzelm:
clarified signature;<br>eliminated aliases of Thm.term_ord;
The file was modified src/HOL/Analysis/normarith.ML (diff)
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
The file was modified src/HOL/Library/positivstellensatz.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
Changeset 67561:f0b11413f1c9 by wenzelm:
clarified signature: prefer proper order operation;
The file was modified src/Doc/Isar_Ref/Generic.thy (diff)
The file was modified src/HOL/Algebra/ringsimp.ML (diff)
The file was modified src/HOL/Mutabelle/mutabelle.ML (diff)
The file was modified src/HOL/Tools/numeral_simprocs.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
Changeset 67560:0fa87bd86566 by wenzelm:
tuned signature: more operations;
The file was modified src/HOL/Algebra/ringsimp.ML (diff)
The file was modified src/HOL/Analysis/normarith.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
The file was modified src/HOL/Library/positivstellensatz.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Nitpick/kodkod.ML (diff)
The file was modified src/HOL/Tools/Nitpick/kodkod_sat.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML (diff)
The file was modified src/HOL/Tools/numeral_simprocs.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/Pure/library.ML (diff)
The file was modified src/Tools/Argo/argo_heap.ML (diff)
The file was modified src/Tools/Argo/argo_simplex.ML (diff)
The file was modified src/Tools/float.ML (diff)
Changeset 67559:833d154ab189 by wenzelm:
clarified signature;
The file was modified src/HOL/Analysis/normarith.ML (diff)
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
The file was modified src/HOL/Library/positivstellensatz.ML (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/Pure/Isar/rule_cases.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)