Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. tuned;
  3. clarified antiquotations;
  4. clarified antiquotations;
  5. discontinued somewhat pointless antiquotations;
  6. NEWS;
  7. clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
  8. clarified antiquotations;
  9. clarified antiquotations;
  10. clarified antiquotations;
  11. clarified antiquotations;
  12. support for "lemma"; support for "schematic" mode; clarified error position;
  13. tuned;
  14. local fixes for "lemma" antiquotation;
  15. clarified signature;
  16. tuned;
  17. clarified keywords: major take precedence for commands, but not used for antiquotations; clarified modules;
  18. tuned modules;
Changeset 74617:08b186726ea0 by wenzelm:
tuned;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74616:997a605b37a9 by wenzelm:
tuned;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74615:9af55a51e185 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/sum_of_squares.ML (diff)
Changeset 74614:c496550dd2c2 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Decision_Procs/langford.ML (diff)
Changeset 74613:6676bf189852 by wenzelm:
discontinued somewhat pointless antiquotations;
The file was modified NEWS (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
Changeset 74612:54085e37ce4d by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 74611:98e7930e6d15 by wenzelm:
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
Changeset 74610:87fc10f5826c by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Meson.thy (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
Changeset 74609:3ef6e38c9847 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Decision_Procs/approximation.ML (diff)
Changeset 74608:cce64b47d13a by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
Changeset 74607:7f6178b655a8 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Library/Rewrite.thy (diff)
The file was modified src/HOL/Library/cconv.ML (diff)
Changeset 74606:40f5c6b2e8aa by wenzelm:
support for &quot;lemma&quot;;<br>support for &quot;schematic&quot; mode;<br>clarified error position;
The file was modified src/Pure/ML/ml_instantiate.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 74605:8b7258c61649 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_instantiate.ML (diff)
Changeset 74604:3da2662a35cd by wenzelm:
local fixes for &quot;lemma&quot; antiquotation;
The file was modified NEWS (diff)
The file was modified src/Doc/Implementation/Logic.thy (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 74603:c22ae7b41bb8 by wenzelm:
clarified signature;
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 74602:722b40f8d764 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_thms.ML (diff)
Changeset 74601:b7804cff55d9 by wenzelm:
clarified keywords: major take precedence for commands, but not used for antiquotations;<br>clarified modules;
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
Changeset 74600:c6610137a092 by wenzelm:
tuned modules;
The file was modified src/Pure/ROOT.ML (diff)