Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. proper latex setup;
  2. tuned;
  3. abbreviations for \<nexists>;
  4. old HOL syntax is for input only;
  5. more PIDE markup;
  6. tuned signature -- clarified modules;
  7. avoid accidental handling of interrupts; interrupts have no properties;
  8. unused;
  9. tuned signature -- clarified modules;
  10. avoid spam in position reports;
  11. tuned signature;
Changeset 62524:bf9a024ca238 by wenzelm:
proper latex setup;
The file was modified src/Doc/Tutorial/document/root.tex (diff)
Changeset 62523:5335e5c53312 by wenzelm:
tuned;
The file was modified src/HOL/Isar_Examples/Cantor.thy (diff)
The file was modified src/HOL/Isar_Examples/Drinker.thy (diff)
Changeset 62522:d32c23d29968 by wenzelm:
abbreviations for \&lt;nexists&gt;;
The file was modified NEWS (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
Changeset 62521:6383440f41a8 by wenzelm:
old HOL syntax is for input only;
The file was modified NEWS (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Hilbert_Choice.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 62520:2382876c238b by wenzelm:
more PIDE markup;
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 62519:a564458f94db by wenzelm:
tuned signature -- clarified modules;
The file was addedsrc/Pure/Concurrent/timeout.ML
The file was modified NEWS (diff)
The file was modified src/HOL/Library/Old_SMT/old_smt_config.ML (diff)
The file was modified src/HOL/Library/refute.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_arith.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_metis.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_refute.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_try0.ML (diff)
The file was modified src/HOL/Mutabelle/mutabelle_extra.ML (diff)
The file was modified src/HOL/Nitpick_Examples/Mono_Nits.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Interpret_Test.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy (diff)
The file was modified src/HOL/TPTP/atp_problem_import.ML (diff)
The file was modified src/HOL/TPTP/atp_theory_export.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_mono.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_util.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/code_prolog.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML (diff)
The file was modified src/HOL/Tools/try0.ML (diff)
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Tools/quickcheck.ML (diff)
The file was modified src/Tools/try.ML (diff)
The file was removedsrc/Pure/Concurrent/time_limit.ML
Changeset 62518:b8efcc9edd7b by wenzelm:
avoid accidental handling of interrupts;<br>interrupts have no properties;
The file was modified src/Pure/ML/exn_properties.ML (diff)
Changeset 62517:091fdc002a52 by wenzelm:
unused;
The file was modified src/Pure/ROOT (diff)
The file was removedsrc/Pure/ML/ml_statistics_dummy.ML
Changeset 62516:5732f1c31566 by wenzelm:
tuned signature -- clarified modules;
The file was modified src/Pure/Isar/runtime.ML (diff)
The file was modified src/Pure/ML/exn_debugger.ML (diff)
The file was modified src/Pure/ML/exn_properties.ML (diff)
The file was modified src/Pure/ML/ml_compiler.ML (diff)
The file was modified src/Pure/ROOT (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was modified src/Pure/Tools/debugger.ML (diff)
The file was removedsrc/Pure/ML/exn_output.ML
Changeset 62515:e73644de5db8 by wenzelm:
avoid spam in position reports;
The file was modified src/HOL/Tools/typedef.ML (diff)
Changeset 62514:aae510e9a698 by wenzelm:
tuned signature;
The file was modified NEWS (diff)
The file was modified src/HOL/Library/bnf_axiomatization.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer_bnf.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/named_target.ML (diff)