Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. tuned example;
  3. added GHC.read_source: read Haskell source text with antiquotations; added "cartouche" antiquotation for ML string expressions as Haskell string literals;
  4. tuned -- prefer GHC.print_codepoint;
  5. support for GHC: string literals;
  6. some support for UTF-8 (similar to Isabelle/Scala version);
  7. clarified signature;
  8. tuned name
  9. add reconstruction by veriT in method smt
  10. split SMT reconstruction into library
Changeset 69213:ab98f058f9dc by wenzelm:
merged
Changeset 69212:be8c70794375 by wenzelm:
tuned example;
The file was modified NEWS (diff)
Changeset 69211:7062639cfdaa by wenzelm:
added GHC.read_source: read Haskell source text with antiquotations;<br>added &quot;cartouche&quot; antiquotation for ML string expressions as Haskell string literals;
The file was modified NEWS (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/Tools/ghc.ML (diff)
Changeset 69210:92fde8f61b0d by wenzelm:
tuned -- prefer GHC.print_codepoint;
The file was modified src/Tools/Code/code_haskell.ML (diff)
Changeset 69209:3f4210c13356 by wenzelm:
support for GHC: string literals;
The file was addedsrc/Pure/Tools/ghc.ML
The file was modified src/Pure/ROOT.ML (diff)
Changeset 69208:3e4edf43e254 by wenzelm:
some support for UTF-8 (similar to Isabelle/Scala version);
The file was addedsrc/Pure/General/utf8.ML
The file was modified src/Pure/ROOT.ML (diff)
Changeset 69207:ae2074acbaa8 by wenzelm:
clarified signature;
The file was modified src/Pure/ML/ml_syntax.ML (diff)
The file was modified src/Pure/Thy/markdown.ML (diff)
The file was modified src/Tools/Code/code_haskell.ML (diff)
The file was modified src/Tools/Code/code_ml.ML (diff)
Changeset 69206:9660bbf5ce7e by nipkow:
tuned name
The file was modified src/HOL/Data_Structures/Array_Braun.thy (diff)
Changeset 69205:8050734eee3e by fleury _mathias.fleury@mpi-inf.mpg.de_:
add reconstruction by veriT in method smt
The file was addedsrc/HOL/Tools/SMT/verit_replay.ML
The file was addedsrc/HOL/Tools/SMT/verit_replay_methods.ML
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/Tools/SMT/conj_disj_perm.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_real.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof_parse.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML (diff)
Changeset 69204:d5ab1636660b by fleury _mathias.fleury@mpi-inf.mpg.de_:
split SMT reconstruction into library
The file was addedsrc/HOL/Tools/SMT/smt_replay.ML
The file was addedsrc/HOL/Tools/SMT/smt_replay_methods.ML
The file was modified src/HOL/SMT.thy (diff)
The file was modified src/HOL/Tools/SMT/z3_real.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay_methods.ML (diff)
The file was removedsrc/HOL/Tools/SMT/z3_replay_util.ML