Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. clarified operations: follow Isabelle/ML more closely;
  2. provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche;
  3. obsolete;
  4. tuned;
  5. clarified name and options for old vampire-4.2.2;
  6. clarified signature;
  7. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
  8. more latex macros;
  9. tuned;
  10. clarified signature;
  11. more antiquotations;
  12. more antiquotations;
  13. more antiquotations;
  14. more antiquotations; more formal use of consts;
  15. more antiquotations; more formal use of consts;
  16. clarified antiquotations;
  17. more antiquotations;
  18. more antiquotations;
  19. more antiquotations;
  20. clarified antiquotation;
  21. more antiquotations;
  22. more antiquotations;
  23. more antiquotations;
  24. tuned;
  25. ML antiquotations for type constructors and term constants;
  26. more antiquotations;
Changeset 74315:30a0f5879d90 by wenzelm:
clarified operations: follow Isabelle/ML more closely;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74314:c645d973f881 by wenzelm:
provide current vampire-4.5.1: presently unused in Sledgehammer, but relevant for Isabelle/Naproche;
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
Changeset 74313:6b998ce1b8cb by wenzelm:
obsolete;
The file was modified src/Pure/Admin/build_vampire.scala
Changeset 74312:7b860fa1140f by wenzelm:
tuned;
The file was modified src/Pure/Admin/build_vampire.scala
Changeset 74311:19022ea3f8cc by wenzelm:
clarified name and options for old vampire-4.2.2;
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Changeset 74310:d7a62db70a07 by wenzelm:
clarified signature;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74309:42523fbf643b by haftmann:
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
The file was modified src/HOL/Bit_Operations.thy
The file was modified src/HOL/Code_Numeral.thy
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/String.thy
Changeset 74308:7466b2a3905a by wenzelm:
more latex macros;
The file was modified lib/texinputs/isabellesym.sty
Changeset 74307:de4b3abaf3ca by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/language_server.scala
Changeset 74306:a117c076aa22 by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Nitpick/kodkod.scala
The file was modified src/Pure/Admin/build_history.scala
The file was modified src/Pure/Admin/ci_profile.scala
The file was modified src/Pure/General/ssh.scala
The file was modified src/Pure/ML/ml_console.scala
The file was modified src/Pure/System/bash.scala
The file was modified src/Pure/System/command_line.scala
The file was modified src/Pure/System/getopts.scala
The file was modified src/Pure/System/process_result.scala
The file was modified src/Pure/Thy/export.scala
The file was modified src/Pure/Tools/build.scala
The file was modified src/Pure/Tools/build_job.scala
The file was modified src/Pure/Tools/server.scala
The file was modified src/Pure/Tools/server_commands.scala
The file was modified src/Tools/VSCode/src/language_server.scala
The file was modified src/Tools/jEdit/src/main.scala
The file was modified src/Tools/jEdit/src/session_build.scala
Changeset 74305:28a582aa25dd by wenzelm:
more antiquotations;
The file was modified src/HOL/HOLCF/Pcpo.thy
The file was modified src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
The file was modified src/HOL/HOLCF/Tools/Domain/domain_induction.ML
The file was modified src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
The file was modified src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
The file was modified src/HOL/HOLCF/Tools/cont_consts.ML
The file was modified src/HOL/HOLCF/Tools/cont_proc.ML
The file was modified src/HOL/HOLCF/Tools/cpodef.ML
The file was modified src/HOL/HOLCF/Tools/domaindef.ML
The file was modified src/HOL/HOLCF/Tools/fixrec.ML
The file was modified src/HOL/HOLCF/Tools/holcf_library.ML
The file was modified src/HOL/HOLCF/ex/Pattern_Match.thy
Changeset 74304:1466f8a2f6dd by wenzelm:
more antiquotations;
The file was modified src/HOL/Hoare/hoare_tac.ML
Changeset 74303:f7ee629b9beb by wenzelm:
more antiquotations;
The file was modified src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
The file was modified src/HOL/Quickcheck_Examples/Hotel_Example.thy
Changeset 74302:6bc96f31cafd by wenzelm:
more antiquotations;<br>more formal use of consts;
The file was modified src/Sequents/Modal0.thy
The file was modified src/Sequents/S43.thy
The file was modified src/Sequents/Sequents.thy
The file was modified src/Sequents/modal.ML
The file was modified src/Sequents/prover.ML
The file was modified src/Sequents/simpdata.ML
Changeset 74301:ffe269e74bdd by wenzelm:
more antiquotations;<br>more formal use of consts;
The file was modified src/FOLP/IFOLP.thy
The file was modified src/FOLP/hypsubst.ML
The file was modified src/FOLP/simp.ML
The file was modified src/FOLP/simpdata.ML
Changeset 74300:33f13d2d211c by wenzelm:
clarified antiquotations;
The file was modified src/FOL/FOL.thy
Changeset 74299:16e5870fe21e by wenzelm:
more antiquotations;
The file was modified src/CTT/CTT.thy
Changeset 74298:45a77ee63e57 by wenzelm:
more antiquotations;
The file was modified src/CCL/Wfd.thy
Changeset 74297:ac130a6bd6b2 by wenzelm:
more antiquotations;
The file was modified src/ZF/arith_data.ML
The file was modified src/ZF/int_arith.ML
Changeset 74296:abc878973216 by wenzelm:
clarified antiquotation;
The file was modified src/ZF/Inductive.thy
The file was modified src/ZF/Tools/datatype_package.ML
The file was modified src/ZF/Tools/inductive_package.ML
The file was modified src/ZF/ind_syntax.ML
The file was modified src/ZF/int_arith.ML
Changeset 74295:9a9326a072bb by wenzelm:
more antiquotations;
The file was modified src/Provers/hypsubst.ML
The file was modified src/Provers/splitter.ML
The file was modified src/Tools/induct.ML
The file was modified src/Tools/misc_legacy.ML
The file was modified src/Tools/nbe.ML
Changeset 74294:ee04dc00bf0a by wenzelm:
more antiquotations;
The file was modified src/ZF/Datatype.thy
The file was modified src/ZF/Tools/datatype_package.ML
The file was modified src/ZF/Tools/induct_tacs.ML
The file was modified src/ZF/Tools/inductive_package.ML
The file was modified src/ZF/Tools/primrec_package.ML
The file was modified src/ZF/Tools/typechk.ML
The file was modified src/ZF/arith_data.ML
The file was modified src/ZF/ind_syntax.ML
The file was modified src/ZF/int_arith.ML
The file was modified src/ZF/simpdata.ML
Changeset 74293:54279cfcf037 by wenzelm:
more antiquotations;
The file was modified src/FOL/fologic.ML
The file was modified src/FOL/simpdata.ML
Changeset 74292:39c98371606f by wenzelm:
tuned;
The file was modified src/HOL/Tools/record.ML
Changeset 74291:b83fa8f3a271 by wenzelm:
ML antiquotations for type constructors and term constants;
The file was modified NEWS
The file was modified etc/symbols
The file was modified src/Pure/ML/ml_antiquotation.ML
The file was modified src/Pure/ML/ml_antiquotations1.ML
The file was modified src/Pure/ML/ml_lex.ML
The file was modified src/Pure/consts.ML
Changeset 74290:b2ad24b5a42c by wenzelm:
more antiquotations;
The file was modified NEWS
The file was modified etc/symbols
The file was modified src/HOL/Decision_Procs/approximation.ML
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
The file was modified src/HOL/Library/cconv.ML
The file was modified src/HOL/Tools/Meson/meson_clausify.ML
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML
The file was modified src/HOL/Tools/hologic.ML
The file was modified src/HOL/Tools/lin_arith.ML
The file was modified src/HOL/Tools/record.ML
The file was modified src/HOL/Tools/sat.ML
The file was modified src/Pure/ML/ml_antiquotations1.ML
The file was modified src/ZF/Tools/inductive_package.ML

Summary

  1. explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
  2. tuned signature, according to Isabelle/28a582aa25dd;
Changeset 12013:33b9d9a97696 by haftmann:
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
The file was modified thys/Native_Word/Word_Type_Copies.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Bits_Int.thy
The file was modified thys/Word_Lib/Generic_set_bit.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
Changeset 12012:a168f8f2bbc3 by wenzelm:
tuned signature, according to Isabelle/28a582aa25dd;
The file was modified thys/Tycon/tycondef.ML