Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. more operations: avoid intermediate list;
  3. discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);
  4. update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;
  5. drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;
  6. tuned;
  7. backout b6aa5eac0a1a;
  8. tuned;
  9. Thm.shared context: speed-up low-level inferences;
  10. tuned whitespace;
  11. backout 4a174bea55e2;
  12. Backed out changeset f34d11942ac1
  13. backout e3fe192fa4a8;
  14. backout 61f652dd955a;
  15. Backed out changeset e3db27e3b0c6
  16. Backed out changeset cd5d56abda10
  17. revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
Changeset 77879:dd222e2af01a by wenzelm:
tuned;
The file was modified src/HOL/Decision_Procs/ferrante_rackoff.ML (diff)
The file was modified src/HOL/Library/cconv.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Nominal/nominal_fresh_fun.ML (diff)
The file was modified src/HOL/Real_Asymp/multiseries_expansion.ML (diff)
The file was modified src/HOL/Statespace/distinct_tree_prover.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/Function/induction_schema.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Function/relation.ML (diff)
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/Quotient/quotient_tacs.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/numeral.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/HOL/Tools/split_rule.ML (diff)
The file was modified src/Provers/Arith/fast_lin_arith.ML (diff)
The file was modified src/Pure/Isar/class_declaration.ML (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/conjunction.ML (diff)
The file was modified src/Pure/drule.ML (diff)
The file was modified src/Pure/ex/Guess.thy (diff)
The file was modified src/Pure/goal.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/ZF/Tools/cartprod.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
Changeset 77878:35a1788dd6f9 by wenzelm:
more operations: avoid intermediate list;
The file was modified src/Pure/term_items.ML (diff)
Changeset 77877:04f0b689981c by wenzelm:
discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892);
The file was modified src/Pure/thm.ML (diff)
Changeset 77876:1d3b3bf5ea3f by wenzelm:
update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter;
The file was modified NEWS (diff)
Changeset 77875:9374e13655e8 by wenzelm:
drop unused Set().ord, which is potentially inefficient due to dict_ord/dest;
The file was modified src/Pure/General/set.ML (diff)
Changeset 77874:c274f52b11ff by wenzelm:
tuned;
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 77873:864c7c684651 by wenzelm:
backout b6aa5eac0a1a;
The file was modified src/Pure/thm.ML (diff)
Changeset 77872:c404695aaf95 by wenzelm:
tuned;
The file was modified src/HOL/Tools/sat.ML (diff)
Changeset 77871:4f9117e6020d by wenzelm:
Thm.shared context: speed-up low-level inferences;
The file was modified src/Pure/sorts.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 77870:92fd8bed5480 by wenzelm:
tuned whitespace;
The file was modified src/Pure/thm.ML (diff)
Changeset 77869:1156aa9db7f5 by wenzelm:
backout 4a174bea55e2;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/compute.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/linker.ML (diff)
The file was modified src/HOL/Types_To_Sets/internalize_sort.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/envir.ML (diff)
The file was modified src/Pure/logic.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/sorts.ML (diff)
The file was modified src/Pure/term_ord.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 77868:6ea0030b9ee9 by wenzelm:
Backed out changeset f34d11942ac1
The file was modified src/Pure/thm.ML (diff)
Changeset 77867:686a7d71ed7b by wenzelm:
backout e3fe192fa4a8;
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/HOL/Examples/Iff_Oracle.thy (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/thm_deps.ML (diff)
Changeset 77866:3bd1aa2f3517 by wenzelm:
backout 61f652dd955a;
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_util.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Pure/thm_deps.ML (diff)
Changeset 77865:6f7a577a1406 by wenzelm:
Backed out changeset e3db27e3b0c6
The file was modified src/Pure/proofterm.ML (diff)
Changeset 77864:11e8f27e741a by wenzelm:
Backed out changeset cd5d56abda10
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 77863:760515c45864 by wenzelm:
revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/compute.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/linker.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
The file was modified src/HOL/Types_To_Sets/local_typedef.ML (diff)
The file was modified src/HOL/Types_To_Sets/unoverloading.ML (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Tools/IsaPlanner/rw_inst.ML (diff)