Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more portable SQL types;
  2. more portable: SQL standard syntax instead of MySQL extension;
  3. general SQL database support, for SQLite and PostgreSQL; tuned;
  4. updated;
  5. minimal support for PostgreSQL databases;
  6. elaborated examples for computations
  7. isabelle update_cartouches
  8. dedicated computation preprocessing rules for nat, int implemented by target language literals
  9. dropped superfluous preprocessing rule
  10. preprocessing rules must always stem from static context
Changeset 65004:fd4d1395fa17 by wenzelm:
more portable SQL types;
The file was modified src/Pure/General/sql.scala (diff)
Changeset 65003:4b4ccf86755c by wenzelm:
more portable: SQL standard syntax instead of MySQL extension;
The file was modified src/Pure/General/sql.scala (diff)
Changeset 65002:0c44e3e9126f by wenzelm:
general SQL database support, for SQLite and PostgreSQL;<br>tuned;
The file was addedsrc/Pure/General/sql_database.scala
The file was modified src/Pure/General/postgresql.scala (diff)
The file was modified src/Pure/General/sqlite.scala (diff)
The file was modified src/Pure/build-jars (diff)
Changeset 65001:d7cefedbca94 by wenzelm:
updated;
The file was modified Admin/components/components.sha1 (diff)
Changeset 65000:b28bd9dfe108 by wenzelm:
minimal support for PostgreSQL databases;
The file was addedsrc/Pure/General/postgresql.scala
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified src/Pure/build-jars (diff)
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)