Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. clarified signature;
  3. proper ml_source: avoid duplicate Bash.string;
  4. misc tuning and clarification: prefer functions over data;
  5. tuned;
  6. misc tuning and clarification;
  7. tuned messages;
  8. tuned;
  9. merged
  10. de-applying and simplifying
Changeset 72279:ae89eac1d332 by wenzelm:
merged
Changeset 72278:199dc903131b by wenzelm:
clarified signature;
The file was modified src/HOL/Library/Sum_of_Squares/sos_wrapper.ML (diff)
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/Pure/General/file.ML (diff)
The file was modified src/Pure/Tools/ghc.ML (diff)
Changeset 72277:48254fa33d88 by wenzelm:
proper ml_source: avoid duplicate Bash.string;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72276:dfe150a246e6 by wenzelm:
misc tuning and clarification: prefer functions over data;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72275:f7189b7f5567 by wenzelm:
tuned;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72274:a1098a183f4a by wenzelm:
misc tuning and clarification;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72273:b8f32e830e95 by wenzelm:
tuned messages;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72272:6931ab4f1a47 by wenzelm:
tuned;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72271:7e90e1d178b5 by paulson:
merged
Changeset 72270:2af901e467da by paulson _lp15@cam.ac.uk_:
de-applying and simplifying
The file was modified src/HOL/Complex_Analysis/Contour_Integration.thy (diff)