Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more messy proofs redone, and new material
  2. merged
  3. merged
  4. new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
  5. merged
  6. tuned -- avoid spurious exception trace for "the";
  7. proof of concept for residue rings over int using type numerals
  8. more correct error message
  9. uniform tagging for printable and non-printable literals
Changeset 68041:d45b78cb86cf by paulson _lp15@cam.ac.uk_:
more messy proofs redone, and new material
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
Changeset 68040:362baebe25a5 by paulson:
merged
Changeset 68039:67b39890158c by paulson:
merged
Changeset 68038:20b713cff87a by paulson _lp15@cam.ac.uk_:
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
Changeset 68037:7eb532e4f8c0 by wenzelm:
merged
Changeset 68036:4c9e79aeadf0 by wenzelm:
tuned -- avoid spurious exception trace for "the";
The file was modified src/Pure/more_thm.ML (diff)
Changeset 68035:6d7cc6723978 by haftmann:
proof of concept for residue rings over int using type numerals
The file was addedsrc/HOL/ex/Residue_Ring.thy
The file was modified src/HOL/ROOT (diff)
Changeset 68034:27ba50c79328 by haftmann:
more correct error message
The file was modified src/Tools/Code/code_scala.ML (diff)
Changeset 68033:ad4b8b6892c3 by haftmann:
uniform tagging for printable and non-printable literals
The file was modified NEWS (diff)
The file was modified src/Doc/Codegen/Adaptation.thy (diff)
The file was modified src/HOL/Library/Code_Test.thy (diff)
The file was modified src/HOL/String.thy (diff)