isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 tip

merged
2023-01-09, by paulson
Substantial de-applying and streamlining
2023-01-09, by paulson
tuned sledgehammer default provers to only include local ones
2023-01-09, by desharna
enforce rebuild of Isabelle/ML to update build databases;
2023-01-06, by wenzelm
prefer relative src_path (if possible) -- in contrast to 9ce0aa145d21:
2023-01-06, by wenzelm
proper treatment of unicode_symbols;
2023-01-06, by wenzelm
tuned signature: avoid alias that is unclear wrt. lazy state and Symbol.encode/decode status;
2023-01-06, by wenzelm
removed unused operation: unclear wrt. Symbol.encode/decode status;
2023-01-06, by wenzelm
tuned signature: more uniform operations;
2023-01-06, by wenzelm
tuned comments;
2023-01-06, by wenzelm
unused;
2023-01-06, by wenzelm
more uniform operations;
2023-01-06, by wenzelm
restrict to proper_session_theories;
2023-01-06, by wenzelm
proper build parameters (amending d858e6f15da3);
2023-01-06, by wenzelm
treat update_options as part of Sessions.Info meta_digest, for proper re-build of updated sessions;
2023-01-06, by wenzelm
more command-line options;
2023-01-06, by wenzelm
tuned options --- avoid confusion with "isabelle build -b";
2023-01-05, by wenzelm
tuned signature;
2023-01-05, by wenzelm
isabelle update -u path_cartouches;
2023-01-05, by wenzelm
merged
2023-01-05, by wenzelm
updated documentation;
2023-01-05, by wenzelm
more options;
2023-01-05, by wenzelm
tuned message;
2023-01-05, by wenzelm
isabelle update no longer uses PIDE dump, but regular session build database: more scalable;
2023-01-05, by wenzelm
more robust;
2023-01-05, by wenzelm
more operations;
2023-01-05, by wenzelm
proper Node.init_blobs, not just edits (amending ca872f20cf5b);
2023-01-05, by wenzelm
tuned signature;
2023-01-05, by wenzelm
tuned signature;
2023-01-05, by wenzelm
clarified session sources: theory and blobs are read from database, instead of physical file-system;
2023-01-05, by wenzelm
tuned;
2023-01-05, by wenzelm
clarified signature: more operations;
2023-01-04, by wenzelm
clarified signature: more operations;
2023-01-04, by wenzelm
tuned;
2023-01-04, by wenzelm
more direct access to session_sources, without somewhat fragile file-system operations;
2023-01-04, by wenzelm
tuned;
2023-01-04, by wenzelm
tuned signature;
2023-01-04, by wenzelm
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
2023-01-04, by wenzelm
clarified signature: old node is ignored;
2023-01-04, by wenzelm
tuned;
2023-01-04, by wenzelm
clarified signature;
2023-01-04, by wenzelm
final tidying of theorems
2023-01-04, by paulson
merged
2023-01-04, by paulson
merged
2023-01-04, by paulson
continued proof simplification
2023-01-04, by paulson
merged
2023-01-03, by paulson
Further simplifications
2023-01-03, by paulson
More tidying of proofs
2023-01-03, by paulson
tuned;
2023-01-04, by wenzelm
merged
2023-01-03, by wenzelm
discontinued fragile operation;
2023-01-03, by wenzelm
more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;
2023-01-03, by wenzelm
tuned whitespace;
2023-01-03, by wenzelm
tuned;
2023-01-03, by wenzelm
avoid somewhat fragile Document.Node.Name.master_dir_path;
2023-01-03, by wenzelm
clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;
2023-01-03, by wenzelm
tuned;
2023-01-03, by wenzelm
clarified modules;
2023-01-03, by wenzelm
tuned;
2023-01-03, by wenzelm
tuned;
2023-01-03, by wenzelm
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
2023-01-03, by wenzelm
tuned signature: avoid too many aliases (see also 72daee8a39ca);
2023-01-03, by wenzelm
clarified modules;
2023-01-03, by wenzelm
merged
2023-01-03, by desharna
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
2022-12-26, by desharna
Fixed a couple of simple_path occurrences
2023-01-03, by paulson
merged
2023-01-02, by paulson
Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"
2023-01-02, by paulson
clarified signature: more explicit types;
2023-01-02, by wenzelm
more robust: prefer internal theory names;
2023-01-02, by wenzelm
clarified session_sources (again, see also 9d0e6ea7aa68);
2023-01-02, by wenzelm
clarified signature: more explicit types;
2023-01-02, by wenzelm
tuned output;
2023-01-02, by wenzelm
clarified signature: more general operations;
2023-01-02, by wenzelm
clarified signature: more explicit types;
2023-01-02, by wenzelm
clarified signature: more explicit types (see also 90c552d28d36);
2023-01-02, by wenzelm
do write_session_sources early, to have information available in build job;
2023-01-02, by wenzelm
tuned signature, following Url.append_path;
2023-01-02, by wenzelm
do not bundle Isabelle/Naproche, while it keeps changing;
2023-01-02, by wenzelm
tuned signature;
2023-01-02, by wenzelm
tuned;
2023-01-02, by wenzelm
clarified signature: uniform master_dir instead of separate field;
2023-01-02, by wenzelm
more standard master_dir;
2023-01-02, by wenzelm
tuned signature, following Url.append_path;
2023-01-01, by wenzelm
merged
2023-01-01, by wenzelm
more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;
2023-01-01, by wenzelm
store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions;
2023-01-01, by wenzelm
tuned signature;
2022-12-31, by wenzelm
tuned;
2022-12-31, by wenzelm
tunes signature;
2022-12-31, by wenzelm
clarified signature;
2022-12-31, by wenzelm
tuned signature;
2022-12-31, by wenzelm
more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;
2022-12-31, by wenzelm
tuned;
2022-12-31, by wenzelm
unused;
2022-12-31, by wenzelm
tuned;
2022-12-31, by wenzelm
clarified modules;
2022-12-31, by wenzelm
tuned: no need to map master_dir, which does not participate in comparison;
2022-12-31, by wenzelm
tuned signature;
2022-12-31, by wenzelm
tuned signature;
2022-12-31, by wenzelm
tuned comments;
2022-12-31, by wenzelm
clarified signature;
2022-12-31, by wenzelm
tuned;
2022-12-31, by wenzelm
removed an unfortunate sledgehammer command
2023-01-01, by paulson
A couple of patches
2023-01-01, by paulson
Big simplifications of old proofs
2023-01-01, by paulson
repaired a proof
2022-12-31, by paulson
Continued proof simplifications
2022-12-30, by paulson
merged
2022-12-30, by paulson
A further round of proof consolidation
2022-12-30, by paulson
tuned signature: avoid too many aliases;
2022-12-30, by wenzelm
proper thread context (amending 01a7265db76b) -- at the danger of blocking the GUI;
2022-12-30, by wenzelm
more robust: avoid detour via somewhat fragile Node.Name.path;
2022-12-30, by wenzelm
clarified generic path operations;
2022-12-30, by wenzelm
more flexible: implicit support for Windows;
2022-12-30, by wenzelm
tuned signature;
2022-12-30, by wenzelm
clarified output;
2022-12-30, by wenzelm
tuned;
2022-12-30, by wenzelm
merged
2022-12-29, by paulson
More tidying
2022-12-29, by paulson