Skip to content
Success

Changes

Summary

  1. more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
  2. more symbols;
Changeset 64557:37074e22e8be by wenzelm:
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/Concurrent/standard_thread.ML (diff)
The file was modified src/Pure/Concurrent/thread_attributes.ML (diff)
The file was modified src/Pure/Tools/ml_process.scala (diff)
Changeset 64556:851ae0e7b09c by wenzelm:
more symbols;
The file was modified etc/symbols (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML (diff)
The file was modified src/Provers/clasimp.ML (diff)
The file was modified src/Provers/classical.ML (diff)
The file was modified src/Provers/splitter.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)
The file was modified src/Pure/General/position.ML (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/ML/ml_antiquotation.ML (diff)
The file was modified src/Pure/ML/ml_compiler0.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_options.ML (diff)
The file was modified src/Pure/ML/ml_print_depth.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
The file was modified src/Pure/Proof/reconstruct.ML (diff)
The file was modified src/Pure/Syntax/ast.ML (diff)
The file was modified src/Pure/Syntax/parser.ML (diff)
The file was modified src/Pure/Syntax/printer.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/Syntax/syntax_trans.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
The file was modified src/Pure/Tools/find_consts.ML (diff)
The file was modified src/Pure/Tools/find_theorems.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/goal.ML (diff)
The file was modified src/Pure/goal_display.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/pattern.ML (diff)
The file was modified src/Pure/pure_syn.ML (diff)
The file was modified src/Pure/pure_thy.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/skip_proof.ML (diff)
The file was modified src/Pure/type_infer.ML (diff)
The file was modified src/Pure/type_infer_context.ML (diff)
The file was modified src/Pure/unify.ML (diff)
The file was modified src/Pure/variable.ML (diff)
The file was modified src/Sequents/prover.ML (diff)
The file was modified src/Tools/intuitionistic.ML (diff)
The file was modified src/ZF/Tools/typechk.ML (diff)