Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuning
  2. preprocess typedefs and quotients correctly
  3. adapted Nunchaku's input syntax to new design decisions
  4. more informative error (see 6e9c22c494c5);
  5. tuned signature -- more friendly for experimentation;
  6. clarified hg push return code: 1 means "nothing to push";
  7. proper Nunchaku setup to use CVC4 and Kodkod
  8. more specific hardware information: relevant for ultimate Mac OS X version;
  9. just one task to identify Isabelle + AFP repository snapshots and build release; report AFP changeset id on website;
  10. tuned;
  11. Deleted spurious markup
  12. latest Mac OS X versions *are* still supported, but presently without formal reference systems;
Changeset 64413:c0d5e78eb647 by blanchet:
tuning
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_tactics.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
Changeset 64412:2ed3da32bf41 by blanchet:
preprocess typedefs and quotients correctly
The file was modified src/HOL/Nunchaku/Tools/nunchaku_collect.ML (diff)
Changeset 64411:0af9926e1303 by blanchet:
adapted Nunchaku's input syntax to new design decisions
The file was modified src/HOL/Nunchaku/Tools/nunchaku_collect.ML (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku_problem.ML (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku_translate.ML (diff)
Changeset 64410:89da169f66fa by wenzelm:
more informative error (see 6e9c22c494c5);
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 64409:70c87ca55f2c by wenzelm:
tuned signature -- more friendly for experimentation;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 64408:50bcf976f276 by wenzelm:
clarified hg push return code: 1 means "nothing to push";
The file was modified src/Pure/General/mercurial.scala (diff)
The file was modified src/Pure/System/process_result.scala (diff)
Changeset 64407:5c5b9d945625 by blanchet:
proper Nunchaku setup to use CVC4 and Kodkod
The file was modified src/HOL/Nunchaku/Nunchaku.thy (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku.ML (diff)
The file was modified src/HOL/Nunchaku/Tools/nunchaku_tool.ML (diff)
Changeset 64406:492de9062cd2 by wenzelm:
more specific hardware information: relevant for ultimate Mac OS X version;
The file was modified Admin/PLATFORMS (diff)
Changeset 64405:81bac77929d9 by wenzelm:
just one task to identify Isabelle + AFP repository snapshots and build release;<br>report AFP changeset id on website;
The file was modified src/Pure/Admin/build_release.scala (diff)
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 64404:d75397e0aad5 by wenzelm:
tuned;
The file was modified Admin/lib/Tools/makedist (diff)
Changeset 64403:7fa053298f67 by paulson _lp15@cam.ac.uk_:
Deleted spurious markup
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
Changeset 64402:4f0acbd97491 by wenzelm:
latest Mac OS X versions *are* still supported, but presently without formal reference systems;
The file was modified Admin/PLATFORMS (diff)