Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid overlapping PIDE markup (amending bb25ea271b15);
  2. recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB);
  3. clarified antiquotations;
  4. merged
  5. clarified antiquotations;
  6. clarified antiquotations;
  7. clarified antiquotations;
  8. clarified antiquotations;
  9. clarified antiquotations;
  10. clarified positions, notably for ML compiler errors;
  11. clarified message;
  12. proper default for Sledgehammer GUI panel;
  13. tuned antiquotations;
  14. more convenient ML arguments: avoid excessive nesting of cartouches;
  15. outer syntax: support for control-cartouche tokens;
  16. merged
  17. An example
  18. prefer veriT over Z3 in sledgehammer
  19. added Zipperposition to sledgehammer's default provers
Changeset 74387:6edb71482de6 by wenzelm:
avoid overlapping PIDE markup (amending bb25ea271b15);
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74386:40804452ab6b by wenzelm:
recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB);
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 74385:04b1ce7efd22 by wenzelm:
clarified antiquotations;
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 74384:bd9a5e128c31 by wenzelm:
merged
Changeset 74383:107941e8fa01 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Pattern_Aliases.thy (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_collect.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/set_comprehension_pointfree.ML (diff)
Changeset 74382:8d0294d877bd by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/SMT/conj_disj_perm.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_real.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_util.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_interface.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/z3_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay_methods.ML (diff)
Changeset 74381:79f484b0e35b by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_countable.ML (diff)
Changeset 74380:79ac28db185c by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_model.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_mono.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_preproc.ML (diff)
Changeset 74379:9ea507f63bcb by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_proof_reconstruct.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_util.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
Changeset 74378:bb25ea271b15 by wenzelm:
clarified positions, notably for ML compiler errors;
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74377:6cefe97cb3ab by wenzelm:
clarified message;
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74376:1cc630940147 by wenzelm:
proper default for Sledgehammer GUI panel;
The file was modified src/HOL/Tools/etc/options (diff)
Changeset 74375:ba880f3a4e52 by wenzelm:
tuned antiquotations;
The file was modified src/CCL/Wfd.thy (diff)
The file was modified src/FOLP/IFOLP.thy (diff)
The file was modified src/HOL/HOLCF/Tools/holcf_library.ML (diff)
The file was modified src/HOL/Hoare/hoare_tac.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Transitive_Closure.thy (diff)
The file was modified src/HOL/Typerep.thy (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
The file was modified src/ZF/Tools/typechk.ML (diff)
The file was modified src/ZF/arith_data.ML (diff)
The file was modified src/ZF/ind_syntax.ML (diff)
Changeset 74374:e585e5a906ba by wenzelm:
more convenient ML arguments: avoid excessive nesting of cartouches;
The file was modified NEWS (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74373:6e4093927dbb by wenzelm:
outer syntax: support for control-cartouche tokens;
The file was modified src/Pure/General/antiquote.ML (diff)
The file was modified src/Pure/General/scan.scala (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Isar/token.scala (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/Thy/document_output.ML (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 74372:90c99974f648 by nipkow:
merged
Changeset 74371:4b9876198603 by nipkow:
An example
The file was modified src/HOL/IMP/Hoare_Total.thy (diff)
Changeset 74370:d8dc8fdc46fc by desharna:
prefer veriT over Z3 in sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML (diff)
Changeset 74369:3301c0d8b560 by desharna:
added Zipperposition to sledgehammer's default provers
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)