Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. NEWS;
  3. more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;
  4. clarified exception -- actually reject denominator = 0;
  5. ML pp for Rat.rat;
  6. clarified string_of_rat operations;
  7. tuned signature;
  8. clarified signature;
  9. prefer rat numberals;
  10. support rat numerals via special antiquotation syntax;
  11. tuned signature;
  12. tuned;
  13. tuned signature;
  14. maintain invariant for exported operation;
  15. prefer more efficient Poly/ML operations, taking care of sign;
  16. ad-hoc overloading for standard operations on type Rat.rat;
  17. rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
Changeset 63213:5c8b500347cd by wenzelm:
merged
Changeset 63212:cc9c1f6a6b88 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 63211:0bec0d1d9998 by wenzelm:
more adhoc overloading;<br>eliminated pointless Rat.eq: this is an equality type;<br>tuned;
The file was modified NEWS (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/Multivariate_Analysis/normarith.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63210:a0685d2b420b by wenzelm:
clarified exception -- actually reject denominator = 0;
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63209:82cd1d481eb9 by wenzelm:
ML pp for Rat.rat;
The file was modified src/Pure/General/rat.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 63208:3251e9dfea91 by wenzelm:
clarified string_of_rat operations;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63207:22bd3341b964 by wenzelm:
tuned signature;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63206:13b67739af09 by wenzelm:
clarified signature;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63205:97b721666890 by wenzelm:
prefer rat numberals;
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.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/Multivariate_Analysis/normarith.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
Changeset 63204:921a5be54132 by wenzelm:
support rat numerals via special antiquotation syntax;
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/ML/ml_lex.scala (diff)
Changeset 63203:c1b15830549e by wenzelm:
tuned signature;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63202:e77481be5c97 by wenzelm:
tuned;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63201:f151704c08e4 by wenzelm:
tuned signature;
The file was modified src/HOL/Decision_Procs/Dense_Linear_Order.thy (diff)
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz_tools.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/Multivariate_Analysis/normarith.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/Provers/Arith/fast_lin_arith.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63200:6eccfe9f5ef1 by wenzelm:
maintain invariant for exported operation;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63199:da38571dd5bd by wenzelm:
prefer more efficient Poly/ML operations, taking care of sign;
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63198:c583ca33076a by wenzelm:
ad-hoc overloading for standard operations on type Rat.rat;
The file was modified NEWS (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/Multivariate_Analysis/normarith.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/Pure/General/rat.ML (diff)
Changeset 63197:af562e976038 by wenzelm:
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
The file was addedsrc/Pure/General/rat.ML
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was removedsrc/Tools/rat.ML