2021-09-21 wenzelm merged
2021-09-21 wenzelm clarified antiquotations;
2021-09-21 wenzelm ML antiquotations for object-logic judgment;
2021-09-21 wenzelm proper Sign.const_typargs via Theory.add_deps_const/Theory.const_dep;
2021-09-21 wenzelm clarified modules;
2021-09-21 wenzelm clarified modules;
2021-09-21 wenzelm more uniform syntax;
2021-09-21 wenzelm permissive identification, e.g. relevant for HOL-SPARK examples running on rsync-clone;
2021-09-20 wenzelm NEWS;
2021-09-20 wenzelm bundle lattice_syntax / no_lattice_syntax supersedes theory HOL-Library.Lattice_Syntax;
2021-09-20 wenzelm localized command 'syntax' and 'no_syntax';
2021-09-20 wenzelm tuned;
2021-09-20 wenzelm clarified signature;
2021-09-20 wenzelm clarified signature;
2021-09-20 desharna merged
2021-09-20 desharna proper constants in TPTP $let binding
2021-09-20 wenzelm more operations from Isabelle/ML;
2021-09-20 wenzelm merged
2021-09-20 wenzelm tuned proofs --- eliminated 'guess';
2021-09-20 wenzelm tuned proofs;
2021-09-20 wenzelm clarified antiquotations;
2021-09-20 desharna proper firstorderization in Sledgehammer
2021-09-19 wenzelm clarified signature;
2021-09-19 wenzelm clarified antiquotations;
2021-09-19 wenzelm clarified signature -- prefer antiquotations (with subtle change of exception content);
2021-09-19 wenzelm more control symbols;
2021-09-19 wenzelm support ML antiquotations with fn abstraction;
2021-09-19 wenzelm unused;
Loading...
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 tip