Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
  2. removed junk;
  3. merged
  4. separated commands from annotations to be able to abstract about the latter only
  5. prefer standard Term.dest_abs, with minor deviation of generated names;
  6. tuned comments;
Changeset 74506:d97c48dc87fa by wenzelm:
support HOL-Isar_Examples.Hoare as well (amending 403ce50e6a2a);
The file was modified src/HOL/Hoare/hoare_tac.ML (diff)
Changeset 74505:ce8152fb021b by wenzelm:
removed junk;
The file was modified src/HOL/Hoare/ExamplesTC.thy (diff)
Changeset 74504:7422950f3955 by nipkow:
merged
Changeset 74503:403ce50e6a2a by nipkow:
separated commands from annotations to be able to abstract about the latter only
The file was modified src/HOL/Hoare/ExamplesTC.thy (diff)
The file was modified src/HOL/Hoare/Hoare_Logic.thy (diff)
The file was modified src/HOL/Hoare/Hoare_Logic_Abort.thy (diff)
The file was modified src/HOL/Hoare/Hoare_Syntax.thy (diff)
The file was modified src/HOL/Hoare/SchorrWaite.thy (diff)
The file was modified src/HOL/Hoare/hoare_syntax.ML (diff)
The file was modified src/HOL/Hoare/hoare_tac.ML (diff)
Changeset 74502:907483081d4c by wenzelm:
prefer standard Term.dest_abs, with minor deviation of generated names;
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
Changeset 74501:0803dd7f920d by wenzelm:
tuned comments;
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)