isabelle: Graph

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

store the {l,g}fp-definition and the monotonicity theorem for inductive predicates (by Jan van Brügge)
18 hours ago, by traytel
make the definition of BNF bounds more easily accessible (by Jan van Brügge)
18 hours ago, by traytel
avoid theorem name clash (by Jan van Brügge)
18 hours ago, by traytel
introduce fewer constants in copy_bnf/lift_bnf (by Jan van Brügge)
18 hours ago, by traytel
Some work on an ancient theory file. And a weird failure in Float.thy
33 hours ago, by paulson
simplified old proofs
33 hours ago, by paulson
polished messy proofs
36 hours ago, by paulson
moved lemmas to book
2 days ago, by nipkow
merged
3 days ago, by wenzelm
tuned messages: more verbosity;
3 days ago, by wenzelm
more explicit default_port;
3 days ago, by wenzelm
tuned messages;
3 days ago, by wenzelm
tuned;
3 days ago, by wenzelm
proper initialization of settings: avoid accidental intrusion from parent process environment;
3 days ago, by wenzelm
clarified solr_data directory, provided via settings;
3 days ago, by wenzelm
explicit settings FIND_FACTS_WEB and option -w, outside of source (immutable) directory;
3 days ago, by wenzelm
tuned message;
3 days ago, by wenzelm
implicit session build, similar to "isabelle export";
3 days ago, by wenzelm
tuned message;
3 days ago, by wenzelm
proper Console_Progress as for other command-line tools;
3 days ago, by wenzelm
tuned messages: more formal;
3 days ago, by wenzelm
clarified signature: progress is usually optional;
3 days ago, by wenzelm
clarified names: "peek" usually refers to evolving mutable state;
3 days ago, by wenzelm
more to check;
3 days ago, by wenzelm
tuned: avoid "open" in ML and "import _" in Scala;
3 days ago, by wenzelm
tuned messages;
3 days ago, by wenzelm
tuned headers;
3 days ago, by wenzelm
more to check;
3 days ago, by wenzelm
clarified names;
3 days ago, by wenzelm
clarified signature and modules;
3 days ago, by wenzelm
tuned;
3 days ago, by wenzelm
avoid conflict with slf4j from sqlite (see also dcddfe4f43a3), notably this message on "isabelle find_facts":
3 days ago, by wenzelm
misc tuning;
3 days ago, by wenzelm
tuned: fewer warnings in IntelliJ IDEA;
3 days ago, by wenzelm
tuned headers;
3 days ago, by wenzelm
tuned headers;
3 days ago, by wenzelm
more NEWS + CONTRIBUTORS;
3 days ago, by wenzelm
tuned comments;
3 days ago, by wenzelm
tool wrappers with specific java options, notably classpath "$SOLR_JARS";
4 days ago, by wenzelm
clarified options;
4 days ago, by wenzelm
proper component src/Tools/Find_Facts;
4 days ago, by wenzelm
components for find_facts;
4 days ago, by wenzelm
suppress duplicate slf4j-api --- already provided by sqlite;
4 days ago, by wenzelm
clarified solr settings;
4 days ago, by wenzelm
proper platform.exe;
4 days ago, by wenzelm
activate admin tools;
4 days ago, by wenzelm
original sources of find-facts 271b5af0c4c8;
4 days ago, by wenzelm
Simplified a lot of messy proofs
3 days ago, by paulson
compatibility with Scala 3
5 days ago, by haftmann
more correct code generation for string literals
5 days ago, by haftmann
made lemma visible
5 days ago, by nipkow
fixed a typo
5 days ago, by paulson
Correction to pretty printing for set intervals, allowing a line break if necessary for a large expression
5 days ago, by paulson
tuned documentation and order of instantiated facts
6 days ago, by Lukas Bartl
merged
6 days ago, by wenzelm
update cygwin near 3.5.5-1, see also https://cygwin.com/pipermail/cygwin-announce/2024-December/012023.html
6 days ago, by wenzelm
direct symbolic implementations of and, or, xor on integer
7 days ago, by haftmann
corrected
6 days ago, by haftmann
merged
7 days ago, by wenzelm
remove special cases for CVC4 that are actually unused (see also 6273d4c8325b and 1f1c5d85d232);
7 days ago, by wenzelm
rebuild cvc5 component (still inactive);
7 days ago, by wenzelm
tuned spacing
7 days ago, by desharna
merged
7 days ago, by desharna
tuned Sledgehammer caching
7 days ago, by desharna
Rename "suggest_of" to "instantiate"
3 weeks ago, by Lukas Bartl
merged
8 days ago, by nipkow
added lemmas
8 days ago, by nipkow
discontinue old / inaccurate show_brackets (see also a4f09493d929 and ca9f5dbab880);
8 days ago, by wenzelm
more markup, notaly for LaTeX output: treat record fields as quasi-consts;
8 days ago, by wenzelm
tuned: more direct string comparison (see also 6e25f82056ad, where the explanation was actually wrong: about fast_string_ord instead of string_ord);
8 days ago, by wenzelm
update release name;
8 days ago, by wenzelm
Added tag Isabelle2025-RC0 for changeset bcb793b951c0
8 days ago, by wenzelm
proper NEWS section; Isabelle2025-RC0
9 days ago, by wenzelm
proper latin "A" instead of greek "Alpha";
9 days ago, by wenzelm
update to current jcef-1.0.61;
9 days ago, by wenzelm
recovered "isabelle component_jcef" from bf537a75e872, adapted to 9fe5d8c70352 and 2a99fcb283ee;
9 days ago, by wenzelm
tuned proofs;
10 days ago, by wenzelm
tuned proofs;
10 days ago, by wenzelm
more robust afp_repository, with regular hgweb URLs;
10 days ago, by wenzelm
more documentation;
10 days ago, by wenzelm
merged
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
tuned (NB: string_ord is required here for its precedence on length);
10 days ago, by wenzelm
more robust: ensure that Nginx is not superseded by implicit Apache dependencies (Ubuntu 24.04);
10 days ago, by wenzelm
tuned NEWS;
10 days ago, by wenzelm
drop obsolete URLs;
10 days ago, by wenzelm
updated Ubuntu versions;
11 days ago, by wenzelm
more robust defaults, notably for Ubuntu 24.04;
11 days ago, by wenzelm
delegate computation to integer thoroughly
11 days ago, by haftmann
merged
11 days ago, by wenzelm
more robust: ensure that /run/sshd is present, which is required for ExecStartPre phase;
11 days ago, by wenzelm
some support for Ubuntu 24.04;
11 days ago, by wenzelm
tuned names: more uniform;
11 days ago, by wenzelm
update NEWS / documentation / descriptions for Phorge (formerly Phabricator);
11 days ago, by wenzelm
unused;
11 days ago, by wenzelm
follow Phorge 2024 week 35;
11 days ago, by wenzelm
separate theory for tests checking bit operations
11 days ago, by haftmann
optionally use shift operations on target numerals for efficient execution
11 days ago, by haftmann
some bit operations on target numerals
11 days ago, by haftmann
rebuild E 3.1 on Windows/Cygwin, with patch for proper interrupts;
12 days ago, by wenzelm
misc tuning and clarification: more explicit types;
13 days ago, by wenzelm
misc tuning and updates for release;
13 days ago, by wenzelm
tuned NEWS;
13 days ago, by wenzelm
provide component cvc5-1.2.0, including arm64-linux;
13 days ago, by wenzelm
refined syntax for code_reserved
2 weeks ago, by haftmann
explicit error message for non-existing code target
2 weeks ago, by haftmann
revert changeset 2f98e3c4592c: avoid conflict with low-level \<^latex> markup;
2 weeks ago, by wenzelm
merged
2 weeks ago, by wenzelm
more robust LaTeX setup, notably for Ubuntu 24.04;
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm
proper treatment of markup within line indentation, notably for Latex.output_ops;
2 weeks ago, by wenzelm
misc tuning and clarification: more explicit types;
2 weeks ago, by wenzelm
more accurate indentation: retain (before: Double) until it is materialized as blanks;
2 weeks ago, by wenzelm
misc tuning: more uniform;
2 weeks ago, by wenzelm
clarified internal data representation, following push/pop model of Scala version;
2 weeks ago, by wenzelm
tuned names;
2 weeks ago, by wenzelm
more accurate formatting of open_block: markup only, without affecting layout (e.g. via force_next);
2 weeks ago, by wenzelm
tuned: more uniform;
2 weeks ago, by wenzelm
proper treatment of XML.Wrapped_Elem as open_block (amending 7cacedbddba7, but this case is presently unused);
2 weeks ago, by wenzelm
tuned;
2 weeks ago, by wenzelm