isabelle: Graph

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

merged
37 hours ago, by nipkow
added Example theory
37 hours ago, by nipkow
merged
37 hours ago, by paulson
Minor lemma tweaking
37 hours ago, by paulson
merged
38 hours ago, by wenzelm
merged
40 hours ago, by wenzelm
tuned output;
41 hours ago, by wenzelm
tuned comments;
41 hours ago, by wenzelm
clarified signature;
42 hours ago, by wenzelm
tuned;
42 hours ago, by wenzelm
avoid tmp files to improve robustness on Windows, where ERROR_PATH_NOT_FOUND has been seen (see also 569135d7352a);
42 hours ago, by wenzelm
tuned signature: more operations (following Isabelle/Scala);
2 days ago, by wenzelm
more operations;
2 days ago, by wenzelm
clarified signature: re-use existing Process_Result.T (NB: err_lines are de-facto program startup errors, anything else is redirected to out_lines);
2 days ago, by wenzelm
tuned signature: more explicit operations;
2 days ago, by wenzelm
tuned output;
2 days ago, by wenzelm
misc tuning;
2 days ago, by wenzelm
tuned Isabelle/ML: more uniform semicolons;
2 days ago, by wenzelm
clarified signature: scalable Bash.input thanks to Bytes.T;
2 days ago, by wenzelm
added time_partial_function command
40 hours ago, by nipkow
A couple of theorems proved by Manuel Eberl from his AFP entry Sum_Of_Squares_Count
2 days ago, by paulson
tuned;
3 days ago, by wenzelm
tuned;
3 days ago, by wenzelm
tuned signature;
3 days ago, by wenzelm
proper Path.print for user output (amending 9498623b27f0);
3 days ago, by wenzelm
tuned signature: more concise access to context data;
3 days ago, by wenzelm
tuned English prose;
3 days ago, by wenzelm
merged
4 days ago, by wenzelm
tuned;
4 days ago, by wenzelm
more uniform cleanup;
4 days ago, by wenzelm
tuned messages;
4 days ago, by wenzelm
more robust: avoid expand_path, which requires "bin/isabelle getenv";
4 days ago, by wenzelm
NEWS;
4 days ago, by wenzelm
enforce fresh build of HOL-Codegenerator_Test;
4 days ago, by wenzelm
more platforms (untested);
4 days ago, by wenzelm
update to mlton-20241230-1 using recent builds from https://sourceforge.net/projects/mlton;
4 days ago, by wenzelm
update to scala-3.3.5;
4 days ago, by wenzelm
update for release;
4 days ago, by wenzelm
Added tag Isabelle2025-RC1 for changeset ba3220909221
4 days ago, by wenzelm
merged
4 days ago, by paulson
nat_diff_split lemmas
4 days ago, by paulson
NEWS
4 days ago, by desharna
tuned whitespace
4 days ago, by desharna
added lemmas ex_terminating_rtranclp_strong and ex_terminating_rtranclp Isabelle2025-RC1
4 days ago, by desharna
added lemma strict_partial_order_wfp_on_finite_set
4 days ago, by desharna
proper order of operations: archive before purge;
5 days ago, by wenzelm
more robust (see also 9601f5582f33);
5 days ago, by wenzelm
tuned spelling;
5 days ago, by wenzelm
clarified NEWS: not user-relevant;
5 days ago, by wenzelm
tuned documentation;
5 days ago, by wenzelm
clarified default of flatlaf.useNativeLibrary=false, for cross-platform GUI uniformity;
5 days ago, by wenzelm
just one flatlaf version: native libraries are optional;
5 days ago, by wenzelm
tuned;
5 days ago, by wenzelm
merged
6 days ago, by Fabian Huch
clarified name;
6 days ago, by Fabian Huch
documentation about Build_Manager;
6 days ago, by Fabian Huch
tuned;
6 days ago, by Fabian Huch
use ssh host for default address;
6 days ago, by Fabian Huch
tuned;
6 days ago, by Fabian Huch
clarified option name;
6 days ago, by Fabian Huch
clarified options: extra ssh connection to cluster of build_manager;
6 days ago, by Fabian Huch
tuned output;
6 days ago, by Fabian Huch
tuned: more standard;
6 days ago, by Fabian Huch
merged;
6 days ago, by wenzelm
more NEWS;
6 days ago, by wenzelm
updated to flatlaf-3.5.4, with fallback on 2.6 for arm64-linux;
6 days ago, by wenzelm
update naproche-20250201: rebuilt executables (just one copy), provide most PDFs;
6 days ago, by wenzelm
tuned whitespace;
6 days ago, by Fabian Huch
documentation about Find_Facts;
6 days ago, by Fabian Huch
more standard: let OS pick random port by default;
6 days ago, by Fabian Huch
clarified platforms;
6 days ago, by Fabian Huch
tuned NEWS;
7 days ago, by wenzelm
merged
7 days ago, by Lukas Stevens
more canonical formatting
7 days ago, by Lukas Stevens
add hook to insert premises in the order solver
7 days ago, by Lukas Stevens
less NEWS (see also afae60d6ff15);
7 days ago, by wenzelm
switch from CVC5 to cvc5, including updates of internal tool references;
4 weeks ago, by wenzelm
more robust wrt. Par_List.map in Browser_Info.build(), see also 2fff9ce6b460 and 787a203a20b6;
8 days ago, by wenzelm
more thorough cleanup;
8 days ago, by wenzelm
more options for build_release: support bundled browser_info and Find_Facts database;
8 days ago, by wenzelm
more standard directory structure;
8 days ago, by wenzelm
tuned output;
8 days ago, by wenzelm
suppress MacOS.jar from jEdit 5.7.0, following 65fd0f032a75;
8 days ago, by wenzelm
tuned GUI: attempt to improve divider mobility;
9 days ago, by wenzelm
rebuild jedit component;
9 days ago, by wenzelm
make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
9 days ago, by wenzelm
more accurate syntax: follow documentation in "isar-ref" (and command 'syntax_consts');
9 days ago, by wenzelm
more robust: make double sure that buffer.getText() is valid (see also 2e7073976c25);
9 days ago, by wenzelm
clarifed terminology
10 days ago, by haftmann
extracted the ^^ subtheory for modularity reasons
10 days ago, by nipkow
tuned
10 days ago, by nipkow
merged
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
minor performance tuning;
10 days ago, by wenzelm
tuned;
10 days ago, by wenzelm
tuned names;
10 days ago, by wenzelm
minor performance tuning: avoid somewhat indirect filter / add_consts;
10 days ago, by wenzelm
clarified signature: more standard map_data;
10 days ago, by wenzelm
misc tuning;
10 days ago, by wenzelm
clarified signature with minor performance tuning: avoid Context.proof_of with its Proof_Context.init_global;
10 days ago, by wenzelm
tuned names;
10 days ago, by wenzelm
more explicit tests for non-PolyML SML platforms
10 days ago, by haftmann
typo
10 days ago, by haftmann
merged
11 days ago, by wenzelm
more NEWS;
11 days ago, by wenzelm
clarified syntax;
11 days ago, by wenzelm
support for "no" polarity of 'adhoc_overloading' vs. 'no_adhoc_overloading';
11 days ago, by wenzelm
more operations;
11 days ago, by wenzelm
clarified signature: proper ML interface to main command, without exposing too many internals;
11 days ago, by wenzelm
tuned signature: more explicit Type.raw_equiv;
11 days ago, by wenzelm
more liberal type equivalence, following thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy from AFP/e69d71bc07c4;
11 days ago, by wenzelm
move theory "HOL-Library.Adhoc_Overloading" to Pure;
11 days ago, by wenzelm
discontinue odd "-build" suffix altogether (see also f51b0b54b20b, bec95e287d26, 6b45a1568637);
12 days ago, by wenzelm
more frugal exports
11 days ago, by haftmann
clarified scopes
11 days ago, by haftmann
more correct SML for SML/NJ
11 days ago, by haftmann
more explicit real operations
11 days ago, by haftmann
merged
12 days ago, by paulson
Tidied
13 days ago, by paulson
merged
12 days ago, by haftmann