Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more antiquotations;
  2. more antiquotations;
  3. more antiquotations;
  4. more antiquotations; more formal use of consts;
  5. more antiquotations; more formal use of consts;
  6. clarified antiquotations;
  7. more antiquotations;
  8. more antiquotations;
  9. more antiquotations;
  10. clarified antiquotation;
  11. more antiquotations;
  12. more antiquotations;
  13. more antiquotations;
  14. tuned;
  15. ML antiquotations for type constructors and term constants;
  16. more antiquotations;
Changeset 74305:28a582aa25dd by wenzelm:
more antiquotations;
The file was modified src/HOL/HOLCF/Pcpo.thy (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_axioms.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_induction.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML (diff)
The file was modified src/HOL/HOLCF/Tools/cont_consts.ML (diff)
The file was modified src/HOL/HOLCF/Tools/cont_proc.ML (diff)
The file was modified src/HOL/HOLCF/Tools/cpodef.ML (diff)
The file was modified src/HOL/HOLCF/Tools/domaindef.ML (diff)
The file was modified src/HOL/HOLCF/Tools/fixrec.ML (diff)
The file was modified src/HOL/HOLCF/Tools/holcf_library.ML (diff)
The file was modified src/HOL/HOLCF/ex/Pattern_Match.thy (diff)
Changeset 74304:1466f8a2f6dd by wenzelm:
more antiquotations;
The file was modified src/HOL/Hoare/hoare_tac.ML (diff)
Changeset 74303:f7ee629b9beb by wenzelm:
more antiquotations;
The file was modified src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy (diff)
The file was modified src/HOL/Quickcheck_Examples/Hotel_Example.thy (diff)
Changeset 74302:6bc96f31cafd by wenzelm:
more antiquotations;<br>more formal use of consts;
The file was modified src/Sequents/Modal0.thy (diff)
The file was modified src/Sequents/S43.thy (diff)
The file was modified src/Sequents/Sequents.thy (diff)
The file was modified src/Sequents/modal.ML (diff)
The file was modified src/Sequents/prover.ML (diff)
The file was modified src/Sequents/simpdata.ML (diff)
Changeset 74301:ffe269e74bdd by wenzelm:
more antiquotations;<br>more formal use of consts;
The file was modified src/FOLP/IFOLP.thy (diff)
The file was modified src/FOLP/hypsubst.ML (diff)
The file was modified src/FOLP/simp.ML (diff)
The file was modified src/FOLP/simpdata.ML (diff)
Changeset 74300:33f13d2d211c by wenzelm:
clarified antiquotations;
The file was modified src/FOL/FOL.thy (diff)
Changeset 74299:16e5870fe21e by wenzelm:
more antiquotations;
The file was modified src/CTT/CTT.thy (diff)
Changeset 74298:45a77ee63e57 by wenzelm:
more antiquotations;
The file was modified src/CCL/Wfd.thy (diff)
Changeset 74297:ac130a6bd6b2 by wenzelm:
more antiquotations;
The file was modified src/ZF/arith_data.ML (diff)
The file was modified src/ZF/int_arith.ML (diff)
Changeset 74296:abc878973216 by wenzelm:
clarified antiquotation;
The file was modified src/ZF/Inductive.thy (diff)
The file was modified src/ZF/Tools/datatype_package.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
The file was modified src/ZF/ind_syntax.ML (diff)
The file was modified src/ZF/int_arith.ML (diff)
Changeset 74295:9a9326a072bb by wenzelm:
more antiquotations;
The file was modified src/Provers/hypsubst.ML (diff)
The file was modified src/Provers/splitter.ML (diff)
The file was modified src/Tools/induct.ML (diff)
The file was modified src/Tools/misc_legacy.ML (diff)
The file was modified src/Tools/nbe.ML (diff)
Changeset 74294:ee04dc00bf0a by wenzelm:
more antiquotations;
The file was modified src/ZF/Datatype.thy (diff)
The file was modified src/ZF/Tools/datatype_package.ML (diff)
The file was modified src/ZF/Tools/induct_tacs.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)
The file was modified src/ZF/Tools/primrec_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)
The file was modified src/ZF/int_arith.ML (diff)
The file was modified src/ZF/simpdata.ML (diff)
Changeset 74293:54279cfcf037 by wenzelm:
more antiquotations;
The file was modified src/FOL/fologic.ML (diff)
The file was modified src/FOL/simpdata.ML (diff)
Changeset 74292:39c98371606f by wenzelm:
tuned;
The file was modified src/HOL/Tools/record.ML (diff)
Changeset 74291:b83fa8f3a271 by wenzelm:
ML antiquotations for type constructors and term constants;
The file was modified NEWS (diff)
The file was modified etc/symbols (diff)
The file was modified src/Pure/ML/ml_antiquotation.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
The file was modified src/Pure/ML/ml_lex.ML (diff)
The file was modified src/Pure/consts.ML (diff)
Changeset 74290:b2ad24b5a42c by wenzelm:
more antiquotations;
The file was modified NEWS (diff)
The file was modified etc/symbols (diff)
The file was modified src/HOL/Decision_Procs/approximation.ML (diff)
The file was modified src/HOL/Library/Sum_of_Squares/positivstellensatz.ML (diff)
The file was modified src/HOL/Library/cconv.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/hologic.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/sat.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
The file was modified src/ZF/Tools/inductive_package.ML (diff)