isabelle: Graph

Moved in some material from the AFP entry Winding_number_eval
23 months ago, by paulson
merged
23 months ago, by wenzelm
tuned messages: less verbosity;
23 months ago, by wenzelm
prefer Other_Isabelle.init instead of adhoc scripts;
23 months ago, by wenzelm
tuned message, following "isabelle components -a";
23 months ago, by wenzelm
clean components more accurately: purge other platforms or archives;
23 months ago, by wenzelm
more operations for SSH.System;
23 months ago, by wenzelm
clarified signature;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
manage other Isabelle distributions via SSH;
23 months ago, by wenzelm
more operations for SSH.System;
23 months ago, by wenzelm
recovered option -C from 092449efcb0e (still required for isabelle_cronjob.scala on Windows), but with slightly different meaning;
23 months ago, by wenzelm
clarified parameters (again);
23 months ago, by wenzelm
Some new material from the AFP
23 months ago, by paulson
clarified defaults: imitate "isabelle components -I" without further parameters;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
merged
23 months ago, by wenzelm
more robust locations (amending 7e11e96a922d) --- notably for cleanup() in build_release, after Admin/ been deleted;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
clarified defaults (see also b310b93563f6);
23 months ago, by wenzelm
tuned comments;
23 months ago, by wenzelm
discontinued adhoc change of environment (from 897f1ac84aab), following ssh c2e8ba15a10a;
23 months ago, by wenzelm
more formal Other_Isabelle.settings, with derived expand_path / bash_path;
23 months ago, by wenzelm
clarified signature: minimal interface for getenv/expand_env, instead of bulky java.util.Map;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
discontinued adhoc change of environment (from c62b99e3ec07), which has been mostly superseded by expand_path / remote_path (from ef6f7e8a018c);
23 months ago, by wenzelm
more operations;
23 months ago, by wenzelm
removed unused user_home argument (see also 897f1ac84aab and 19b6091c2137);
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
more robust: self-contained Other_Isabelle.isabelle_home;
23 months ago, by wenzelm
more robust and uniform Other_Isabelle.scala_build;
23 months ago, by wenzelm
tuned;
23 months ago, by wenzelm
tuned message;
23 months ago, by wenzelm
more robust (see also 7f55a3e28c88): resolve components from current Isabelle context, using Isabelle/Scala instead of shell scripts;
23 months ago, by wenzelm
more strict;
23 months ago, by wenzelm
tuned signature;
23 months ago, by wenzelm
proper ssh.bash_path;
23 months ago, by wenzelm
merged
23 months ago, by desharna
added lemma irreflp_on_multpHO[simp]
24 months ago, by desharna
added lemmas totalp_on_multpDM, totalp_multpDM, totalp_on_multpHO, and totalp_multpHO
24 months ago, by desharna
Beautifying an old entry
23 months ago, by paulson
generalized theory name: euclidean division denotes one particular division definition on integers
23 months ago, by haftmann
merged
24 months ago, by wenzelm
support remote operations;
24 months ago, by wenzelm
more elementary command-line, following lib/Tools/components;
24 months ago, by wenzelm
clarified defaults;
24 months ago, by wenzelm
more accurate options (amending 7e19dc018db9);
24 months ago, by wenzelm
clarified defaults;
24 months ago, by wenzelm
support remote download_file;
24 months ago, by wenzelm
more modular shell script;
24 months ago, by wenzelm
more uniform options for "curl", following lib/Tools/components;
24 months ago, by wenzelm
tuned: drop redundant "expand";
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
added lemmas total_on_mult, total_mult, totalp_on_multp, and totalp_multp
24 months ago, by desharna
proper name for lemma totalp_on_total_on_eq
24 months ago, by desharna
update to jdk-17.0.6;
24 months ago, by wenzelm
proper cleanup;
24 months ago, by wenzelm
avoid odd suffix in published HTML library;
24 months ago, by wenzelm
tuned signature: avoid aliases;
24 months ago, by wenzelm
tuned message;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned signature;
24 months ago, by wenzelm
clarified modules (again, in contrast to f8f065e20837);
24 months ago, by wenzelm
support IPC via database server;
24 months ago, by wenzelm
proper signature;
24 months ago, by wenzelm
support specific connection types, for additional operations;
24 months ago, by wenzelm
more correct and complete bibliography;
24 months ago, by wenzelm
tuned signature;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
proper position for semantic completion: avoid duplicate quotes;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
proper positions for Isabelle/ML, instead of Isabelle/Scala;
24 months ago, by wenzelm
dismantle special treatment of citations in Isabelle/Scala;
24 months ago, by wenzelm
more direct check of bibtex entries via Isabelle/Scala;
24 months ago, by wenzelm
support Session argument for Scala.Fun;
24 months ago, by wenzelm
obsolete (see also 01c9b3033036);
24 months ago, by wenzelm
proper citations for unselected theories, notably for the default selection of the GUI panel;
24 months ago, by wenzelm
tuned signature;
24 months ago, by wenzelm
more robust theory_source -- in contrast to node_source from fffb978dd683: theory name is more reliable than Document.Node.Name, explicit unicode_symbols;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
merged
24 months ago, by wenzelm
clarified "selected" status;
24 months ago, by wenzelm
uniform keywords for embedded syntax;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
tuned signature;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
more complete index;
24 months ago, by wenzelm
tuned comments;
24 months ago, by wenzelm
parse citations from raw source, without formal context;
24 months ago, by wenzelm
tuned signature: fewer warnings in IntelliJ IDEA;
24 months ago, by wenzelm
tuned messages;
24 months ago, by wenzelm
tuned GUI;
24 months ago, by wenzelm
clarified signature;
24 months ago, by wenzelm
more efficient, thanks to persistent lazy data in Document.Node;
24 months ago, by wenzelm
proper line positions for PIDE document;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
HOL/Library/BigO is obsolete
24 months ago, by paulson
merged
24 months ago, by paulson
tidy up of this messy and obsolete theory
24 months ago, by paulson
clarified file positions: retain original source path;
24 months ago, by wenzelm
backed out changeset 7f7d5c93e36b: no longer required thanks to 9096703ed99e;
24 months ago, by wenzelm
clarified formal check of bibtex entries (again), see also 86a099f896fc and 467f45e79ff9;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
tuned GUI;
24 months ago, by wenzelm
permissive treatment of citations before the theory header: avoid too many changes in AFP;
24 months ago, by wenzelm
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
24 months ago, by wenzelm
clarified documentation: avoid odd speculations about PIDE;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
clarified modules;
24 months ago, by wenzelm
merged
24 months ago, by wenzelm
more complete Bibtex database;
24 months ago, by wenzelm
proper theory context for formal citations;
24 months ago, by wenzelm
isabelle update -u cite;
24 months ago, by wenzelm
clarified treatment of cite macro name;
24 months ago, by wenzelm
explicit legacy_feature;
24 months ago, by wenzelm
more robust: rely on PIDE markup instead of regex guess;
24 months ago, by wenzelm
more index entries;
24 months ago, by wenzelm
updated documentation;
24 months ago, by wenzelm
clarified names;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
clarified options and defaults: avoid accidental changed of base logic due to augment_options(update_options);
24 months ago, by wenzelm
update documentation: prefer control-symbol-cartouche form of "cite" antiquotations;
24 months ago, by wenzelm
tuned;
24 months ago, by wenzelm
proper language context;
24 months ago, by wenzelm
proper normal form of adjacent XML.Text, notably for Bibtex.update_cite;
24 months ago, by wenzelm
tuned whitespace;
24 months ago, by wenzelm
more robust;
24 months ago, by wenzelm
basic support for update_cite_commands;
24 months ago, by wenzelm
more operations: use proper constants;
24 months ago, by wenzelm
proper session_options (amending da13da82f6f9);
24 months ago, by wenzelm
tuned signature;
24 months ago, by wenzelm
tuned;
24 months ago, 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
24 months ago, by paulson
Missing theorem restored
24 months ago, by paulson
Tidying up BNF
24 months ago, 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