Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. fixing more messy proofs
  3. more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
  4. eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);
  5. proper datatype for 8-bit characters
  6. corrected nonsense
  7. less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
  8. clarified modules;
Changeset 68032:412fe0623c5d by paulson:
merged
Changeset 68031:eda52f4cd4e4 by paulson _lp15@cam.ac.uk_:
fixing more messy proofs
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
Changeset 68030:0a6d6ba383dc by wenzelm:
more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;
The file was modified src/Pure/proofterm.ML (diff)
Changeset 68029:df9044efd054 by wenzelm:
eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);
The file was modified src/Pure/Isar/locale.ML (diff)
Changeset 68028:1f9f973eed2a by haftmann:
proper datatype for 8-bit characters
The file was addedsrc/HOL/Tools/literal.ML
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Adaptation.thy (diff)
The file was modified src/Doc/Codegen/Computations.thy (diff)
The file was modified src/HOL/Code_Evaluation.thy (diff)
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/Imperative_HOL/Heap_Monad.thy (diff)
The file was modified src/HOL/Imperative_HOL/ex/SatChecker.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
The file was modified src/HOL/Library/Char_ord.thy (diff)
The file was modified src/HOL/Library/Code_Target_Int.thy (diff)
The file was modified src/HOL/Library/Code_Target_Nat.thy (diff)
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/Library/Countable.thy (diff)
The file was modified src/HOL/Library/Predicate_Compile_Alternative_Defs.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Parity.thy (diff)
The file was modified src/HOL/Quickcheck_Exhaustive.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/Statespace/state_fun.ML (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/numeral.ML (diff)
The file was modified src/HOL/Tools/string_syntax.ML (diff)
The file was modified src/HOL/ex/Cartouche_Examples.thy (diff)
The file was modified src/Pure/General/integer.ML (diff)
The file was modified src/Tools/Code/code_haskell.ML (diff)
The file was modified src/Tools/Code/code_ml.ML (diff)
The file was modified src/Tools/Code/code_printer.ML (diff)
The file was modified src/Tools/Code/code_scala.ML (diff)
The file was removedsrc/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
The file was removedsrc/HOL/Library/Code_Char.thy
The file was removedsrc/HOL/Tools/string_code.ML
Changeset 68027:64559e1ca05b by haftmann:
corrected nonsense
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
Changeset 68026:a8ee8e4884ec by wenzelm:
less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);
The file was modified src/Pure/proofterm.ML (diff)
Changeset 68025:7fb7a6366a40 by wenzelm:
clarified modules;
The file was modified src/Pure/Concurrent/multithreading.ML (diff)
The file was modified src/Pure/System/isabelle_process.ML (diff)
The file was modified src/Pure/goal.ML (diff)