Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified antiquotations;
  2. clarified antiquotations;
  3. clarified antiquotations;
  4. clarified partial application: immediate check of object-logic, and avoidance of context within closure;
  5. merged
  6. clarified antiquotations;
  7. ML antiquotations for object-logic judgment;
  8. proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
  9. clarified modules;
  10. clarified modules;
  11. more uniform syntax;
  12. permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
  13. NEWS;
  14. bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
  15. localized command 'syntax' and 'no_syntax';
  16. tuned;
  17. clarified signature;
  18. clarified signature;
Changeset 74347:f984d30cd0c3 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/Metis/metis_generate.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Metis/metis_tactic.ML (diff)
Changeset 74346:55007a70bd96 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/Meson/meson.ML (diff)
The file was modified src/HOL/Tools/Meson/meson_clausify.ML (diff)
Changeset 74345:e5ff77db6f38 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Transitive_Closure.thy (diff)
The file was modified src/HOL/Typerep.thy (diff)
Changeset 74344:1c2c0380d58b by wenzelm:
clarified partial application: immediate check of object-logic, and avoidance of context within closure;
The file was modified src/Pure/Isar/object_logic.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74343:e0c072a13771 by wenzelm:
merged
Changeset 74342:5d411d85da8c by wenzelm:
clarified antiquotations;
The file was modified src/FOL/IFOL.thy (diff)
The file was modified src/FOL/fologic.ML (diff)
The file was modified src/ZF/Tools/datatype_package.ML (diff)
The file was modified src/ZF/Tools/ind_cases.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/arith_data.ML (diff)
The file was modified src/ZF/ind_syntax.ML (diff)
Changeset 74341:edf8b141a8c4 by wenzelm:
ML antiquotations for object-logic judgment;
The file was modified NEWS (diff)
The file was modified etc/symbols (diff)
The file was modified lib/texinputs/isabellesym.sty (diff)
The file was modified src/Pure/Isar/object_logic.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74340:e098fa45bfe0 by wenzelm:
proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
The file was modified src/Pure/Isar/object_logic.ML (diff)
Changeset 74339:bff865939cc3 by wenzelm:
clarified modules;
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/Pure/theory.ML (diff)
Changeset 74338:534b231ce041 by wenzelm:
clarified modules;
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 74337:9c1ad2f04660 by wenzelm:
more uniform syntax;
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Main.thy (diff)
Changeset 74336:7bb0ac635397 by wenzelm:
permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
The file was modified src/Pure/System/isabelle_system.ML (diff)
The file was modified src/Pure/System/isabelle_system.scala (diff)
Changeset 74335:eb54c0604ca5 by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 74334:ead56ad40e15 by wenzelm:
bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
The file was modified src/Doc/Main/Main_Doc.thy (diff)
The file was modified src/Doc/Typeclass_Hierarchy/Setup.thy (diff)
The file was modified src/HOL/Examples/Knaster_Tarski.thy (diff)
The file was modified src/HOL/Library/Combine_PER.thy (diff)
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)
The file was modified src/HOL/Library/Library.thy (diff)
The file was modified src/HOL/Library/Option_ord.thy (diff)
The file was modified src/HOL/Main.thy (diff)
The file was removedsrc/HOL/Library/Lattice_Syntax.thy
Changeset 74333:a9b20bc32fa6 by wenzelm:
localized command 'syntax' and 'no_syntax';
The file was modified src/Doc/Isar_Ref/Inner_Syntax.thy (diff)
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 74332:78c1699c7672 by wenzelm:
tuned;
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 74331:b9a3d2fb53e0 by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74330:d882abae3379 by wenzelm:
clarified signature;
The file was modified src/Pure/Proof/proof_syntax.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/Pure/sign.ML (diff)