isabelle: Graph

isabelle update -u cite;
2023-01-15, by wenzelm
clarified treatment of cite macro name;
2023-01-15, by wenzelm
explicit legacy_feature;
2023-01-15, by wenzelm
more robust: rely on PIDE markup instead of regex guess;
2023-01-15, by wenzelm
more index entries;
2023-01-15, by wenzelm
updated documentation;
2023-01-15, by wenzelm
clarified names;
2023-01-15, by wenzelm
tuned;
2023-01-15, by wenzelm
clarified options and defaults: avoid accidental changed of base logic due to augment_options(update_options);
2023-01-15, by wenzelm
update documentation: prefer control-symbol-cartouche form of "cite" antiquotations;
2023-01-14, by wenzelm
tuned;
2023-01-14, by wenzelm
proper language context;
2023-01-14, by wenzelm
proper normal form of adjacent XML.Text, notably for Bibtex.update_cite;
2023-01-14, by wenzelm
tuned whitespace;
2023-01-14, by wenzelm
more robust;
2023-01-14, by wenzelm
basic support for update_cite_commands;
2023-01-14, by wenzelm
more operations: use proper constants;
2023-01-14, by wenzelm
proper session_options (amending da13da82f6f9);
2023-01-14, by wenzelm
tuned signature;
2023-01-14, by wenzelm
tuned;
2023-01-14, by wenzelm
clarified types;
2023-01-13, by wenzelm
more explicit language context;
2023-01-13, by wenzelm
clarified signature: more explicit types;
2023-01-13, by wenzelm
support embedded syntax, for use with control symbols;
2023-01-13, by wenzelm
tuned;
2023-01-13, by wenzelm
tuned;
2023-01-13, by wenzelm
clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
2023-01-13, by wenzelm
more "cite" antiquotations;
2023-01-13, by wenzelm
clarified signature: more generic operations;
2023-01-13, by wenzelm
clarified check: this could be \nocite;
2023-01-13, by wenzelm
avoid confusion of markup element vs. property names;
2023-01-12, by wenzelm
clarified Latex markup: optional cite "location" consists of nested document text;
2023-01-12, by wenzelm
more explicit latex markup;
2023-01-12, by wenzelm
follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;
2023-01-11, by wenzelm
One messy, messy proof
2023-01-15, by paulson
Missing theorem restored
2023-01-14, by paulson
Tidying up BNF
2023-01-14, by paulson
More cleaning up proofs, plus a TeX fix
2023-01-13, by paulson
Fixed a broken proof
2023-01-13, by paulson
Substantial simplification of HOL-Cardinals
2023-01-13, by paulson
merged
2023-01-13, by paulson
Trying to clean up HOL/Cardinals
2023-01-12, by paulson
added session to mirabelle output directory structure
2023-01-12, by desharna
More tidying of topology proofs
2023-01-11, by paulson
Partial round of clearing up applys, etc
2023-01-11, by paulson
merged
2023-01-10, by paulson
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
Further cleaning up of messy proofs
2022-12-29, by paulson
merged
2022-12-29, by paulson
reorganisation and simplification of theorems about transcendental functions
2022-12-29, by paulson
tuned signature;
2022-12-29, by wenzelm
support asynchronous presentation commands, but not for "no_update" / "Keep", which is usually forked via "Toplevel.diag";
2022-12-29, by wenzelm
tuned whitespace;
2022-12-29, by wenzelm
clarified signature;
2022-12-29, by wenzelm
clarified signature;
2022-12-29, by wenzelm
tuned;
2022-12-29, by wenzelm
tuned;
2022-12-29, by wenzelm
discontinued somewhat pointless exception FAILURE with its "alt_state", which was originally due to quasi-mutable states (see 169e5b07ec06);
2022-12-29, by wenzelm
tuned --- more robust ML patterns;
2022-12-29, by wenzelm
tuned;
2022-12-29, by wenzelm
merged
2022-12-28, by wenzelm
tuned signature, for the sake of AFP/Isabelle_C;
2022-12-28, by wenzelm
more uniform report of Markup.language_path;
2022-12-28, by wenzelm
omit pointless guard: ultimately observed by Isabelle_Process.report_message;
2022-12-28, by wenzelm
tuned signature;
2022-12-28, by wenzelm
clarified modules;
2022-12-28, by wenzelm
tuned;
2022-12-28, by wenzelm
tuned signature;
2022-12-28, by wenzelm
tuned;
2022-12-28, by wenzelm
tuned;
2022-12-28, by wenzelm
tuned output;
2022-12-28, by wenzelm
merged
2022-12-28, by paulson
Tidied some messy proofs
2022-12-28, by paulson
merged
2022-12-27, by wenzelm
clarified modules: avoid duplication;
2022-12-27, by wenzelm
tuned output;
2022-12-27, by wenzelm
support for generic File_Format.parse_data, with persistent result in document model;
2022-12-27, by wenzelm
omit warning: somewhat pointless and out-of-context;
2022-12-27, by wenzelm
clarified signature: avoid case class with mutable state;
2022-12-27, by wenzelm
tuned;
2022-12-27, by wenzelm
clarified signature: more explicit types;
2022-12-27, by wenzelm
merged
2022-12-27, by paulson
tidied some messy old proofs
2022-12-27, by paulson
tuned signature;
2022-12-26, by wenzelm
merged
2022-12-26, by wenzelm
tuned signature;
2022-12-26, by wenzelm
more robust;
2022-12-26, by wenzelm
clarified signature: more position information via node_name;
2022-12-26, by wenzelm
tuned signature: avoid name confusion;
2022-12-26, by wenzelm
more bibtex errors;
2022-12-26, by wenzelm
clarified signature: internalize errors (but: the parser rarely fails);
2022-12-26, by wenzelm
tuned signature;
2022-12-26, by wenzelm
clarified signature: more explicit types;
2022-12-26, by wenzelm
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
2022-12-26, by wenzelm
merged
2022-12-26, by desharna
removed old lemma names
2022-12-26, by desharna
merged
2022-12-24, by paulson
merged
2022-12-23, by paulson
A few new Sup/Inf lemmas
2022-12-22, by paulson
clarified messages;
2022-12-24, by wenzelm
tuned signature: follow terminology of VSCode_Resources;
2022-12-24, by wenzelm
tuned signature;
2022-12-23, by wenzelm
tuned signature;
2022-12-23, by wenzelm
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
2022-12-23, by wenzelm
update URL;
2022-12-23, by wenzelm
clarified signature;
2022-12-23, by wenzelm
tuned;
2022-12-23, by wenzelm
tuned;
2022-12-23, by wenzelm
tuned;
2022-12-23, by wenzelm
tuned;
2022-12-23, by wenzelm
tuned;
2022-12-23, by wenzelm
clarified signature: more explicit types;
2022-12-23, by wenzelm
merged
2022-12-23, by desharna
merged
2022-12-22, by desharna
used transp_on in assumptions of lemmas Multiset.bex_(least|greatest)_element
2022-12-20, by desharna
added lemma trans_on_lex_prod[simp]
2022-12-19, by desharna
strengthened and renamed lemma trans_converse and added lemma transp_on_conversep
2022-12-19, by desharna
strengthened and renamed trans_reflclI
2022-12-19, by desharna
strengthened and renamed transp_reflclp
2022-12-19, by desharna
strengthened and renamed lemmas preorder.transp_(ge|gr|le|less)
2022-12-19, by desharna
added lemmas trans_on_subset and transp_on_subset
2022-12-19, by desharna