Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. elaborated examples for computations
  2. isabelle update_cartouches
  3. dedicated computation preprocessing rules for nat, int implemented by target language literals
  4. dropped superfluous preprocessing rule
  5. preprocessing rules must always stem from static context
Changeset 64999:f8f76a501d25 by haftmann:
elaborated examples for computations
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
Changeset 64998:d51478d6aae4 by haftmann:
isabelle update_cartouches
The file was modified src/HOL/Decision_Procs/Algebra_Aux.thy (diff)
The file was modified src/HOL/Decision_Procs/Conversions.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
Changeset 64997:067a6cca39f0 by haftmann:
dedicated computation preprocessing rules for nat, int implemented by target language literals
The file was modified src/HOL/Library/Code_Target_Int.thy (diff)
The file was modified src/HOL/Library/Code_Target_Nat.thy (diff)
Changeset 64996:b316cd527a11 by haftmann:
dropped superfluous preprocessing rule
The file was modified src/HOL/Int.thy (diff)
Changeset 64995:a7af4045f873 by haftmann:
preprocessing rules must always stem from static context
The file was modified src/Tools/Code/code_runtime.ML (diff)