Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
  2. tuned;
  3. added postorder
  4. tuned
Changeset 64927:a5a09855e424 by boehmes:
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/ex/Argo_Examples.thy (diff)
The file was modified src/Tools/Argo/argo_cc.ML (diff)
The file was modified src/Tools/Argo/argo_expr.ML (diff)
The file was modified src/Tools/Argo/argo_proof.ML (diff)
The file was modified src/Tools/Argo/argo_rewr.ML (diff)
The file was modified src/Tools/Argo/argo_simplex.ML (diff)
The file was modified src/Tools/Argo/argo_solver.ML (diff)
The file was modified src/Tools/Argo/argo_thy.ML (diff)
Changeset 64926:75ee8475c37e by wenzelm:
tuned;
The file was modified src/Doc/Isar_Ref/Proof.thy (diff)
Changeset 64925:5eda89787621 by nipkow:
added postorder
The file was modified src/HOL/Library/Tree.thy (diff)
Changeset 64924:a410e8403957 by nipkow:
tuned
The file was modified src/HOL/Library/Tree.thy (diff)