Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified antiquotations;
  2. more robust subgoal addressing;
  3. proper subgoal addressing;
  4. clarified antiquotations;
  5. recursive find_eq, not find_dist;
  6. misc tuning and clarification;
  7. clarified antiquotations;
  8. order_tac: prevent potential bug, improve perf and tracing - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p.
  9. misc tuning and clarification;
  10. clarified antiquotations;
  11. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
  12. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
  13. avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
  14. added Thm.instantiate_beta; tuned;
  15. moved generic implementation into HOL-Main
Changeset 74632:8ab92e40dde6 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Analysis/measurable.ML (diff)
Changeset 74631:f1099c7330b7 by wenzelm:
more robust subgoal addressing;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74630:779ae499ca8b by wenzelm:
proper subgoal addressing;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74629:9264ef3a2ba3 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74628:cd030003efa8 by wenzelm:
recursive find_eq, not find_dist;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74627:c690435c47ee by wenzelm:
misc tuning and clarification;
The file was modified src/HOL/Analysis/metric_arith.ML (diff)
Changeset 74626:9a1f4a7ddf9e by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Analysis/normarith.ML (diff)
Changeset 74625:e6f0c9bf966c by lukas stevens _mail@lukas-stevens.de_:
order_tac: prevent potential bug, improve perf and tracing<br><br>- We need to be careful when the order operators contain schematic variables, e.g. &lt;= = ccw&#039; ?p.
The file was modified src/Provers/order_procedure.ML (diff)
The file was modified src/Provers/order_tac.ML (diff)
Changeset 74624:c2bc0180151a by wenzelm:
misc tuning and clarification;
The file was modified src/HOL/Library/cconv.ML (diff)
Changeset 74623:9b1d33c7bbcc by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (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)
Changeset 74622:9568db8f4882 by wenzelm:
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74621:82ff15b980e9 by wenzelm:
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74620:d622d1dce05c by wenzelm:
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
The file was modified src/Pure/ML/ml_instantiate.ML (diff)
Changeset 74619:e495ab64c694 by wenzelm:
added Thm.instantiate_beta;<br>tuned;
The file was modified NEWS (diff)
Changeset 74618:43142ac556e6 by haftmann:
moved generic implementation into HOL-Main
The file was modified src/HOL/Bit_Operations.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Generate_Target_Nat.thy (diff)