isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

clarified command arguments: optionally restrict to given theories (from theory loader);
17 months ago, by wenzelm
tuned signature: more operations for formal theory context vs. theory loader;
17 months ago, by wenzelm
added Isar command 'print_context_tracing';
17 months ago, by wenzelm
avoid confusion: this is merely about "isabelle dotnet_setup", no codegen yet;
17 months ago, by wenzelm
avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer
17 months ago, by blanchet
merged
17 months ago, by paulson
some refinements in Algebra and Number_Theory
17 months ago, by paulson
provide Go component
17 months ago, by Lars Hupel
merged
17 months ago, by paulson
A subtle fix involving the "measurable" attribute
17 months ago, by paulson
merged
17 months ago, by paulson
Numerous minor tweaks and simplifications
17 months ago, by paulson
substantial tidy-up, shortening many proofs
17 months ago, by paulson
add Go component
17 months ago, by Lars Hupel
backed out changeset 2a26d423d9fb: build_log_database not run yet, so this tests the same changesets again;
17 months ago, by wenzelm
back to post-release mode -- after fork point;
18 months ago, by wenzelm
Added tag Isabelle2023-RC3 for changeset f5fb5bb2533f
18 months ago, by wenzelm
clarified option name (see also ff43a524aa5d);
18 months ago, by wenzelm
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
18 months ago, by wenzelm
more robust: atomic file-system result via tmp file;
18 months ago, by wenzelm
removed junk (amending 8cd399b25dac);
18 months ago, by wenzelm
more robust wrt. undefined state;
18 months ago, by wenzelm
more informative error;
18 months ago, by wenzelm
more robust;
18 months ago, by wenzelm
tuned signature;
18 months ago, by wenzelm
clarified signature: more explicit types;
18 months ago, by wenzelm
more informative shasum: show differences explicitly;
18 months ago, by wenzelm
tuned messages;
18 months ago, by wenzelm
more robust ancestor_results: avoid total existence failure after build_process has crashed elsewhere;
18 months ago, by wenzelm
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
18 months ago, by wenzelm
merged
18 months ago, by nipkow
improved simp rule insert_Times_insert (following Dominique Unruh).
18 months ago, by nipkow
afford multiple tests for arm64_32-darwin on this fast machine;
18 months ago, by wenzelm
proper history_base for AMR64;
18 months ago, by wenzelm
tuned
18 months ago, by nipkow
more robust support for ARM64 platform;
18 months ago, by wenzelm
proper support for Apple Silicon (ARM64);
18 months ago, by wenzelm
merged
18 months ago, by wenzelm
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
18 months ago, by wenzelm
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
18 months ago, by wenzelm
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
18 months ago, by wenzelm
made another two tactics more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
18 months ago, by traytel
made tactic more robust in presence of BNFs nesting live variables (reported by Wolfgang Jeltsch)
18 months ago, by traytel
systematic testing of arm64_32-darwin;
18 months ago, by wenzelm
more hardware details;
18 months ago, by wenzelm
update to polyml-219e0a248f70, with more robust support for ARM64;
18 months ago, by wenzelm
tuned generated README;
18 months ago, by wenzelm
merged
18 months ago, by paulson
Tidied up more messy proofs
18 months ago, by paulson
hints on "hg bisect";
18 months ago, by wenzelm
no hardwired timeout in Isabelle distribution (unlike on AFP): reverting part of 74c75da4cb01 -- without further tinkering it breaks isabelle_cronjob builds;
18 months ago, by wenzelm
Removal of ugly old proofs
18 months ago, by paulson
merged
18 months ago, by paulson
More cosmetic changes
18 months ago, by paulson
Cosmetic polishing of proofs
18 months ago, by paulson
remove debug printing
18 months ago, by Mathias Fleury
merged
18 months ago, by nipkow
added mbox-like latex sugar
18 months ago, by nipkow
Added tag Isabelle2023-RC2 for changeset 53b59fa42696
18 months ago, by wenzelm
prefer Output.writeln for theory "results", as opposed to Output.state for genuine proof states (see f8c412a45af8, c668735fb8b5, ecf80e37ed1a);
18 months ago, by wenzelm
revert adhoc change ab9cc7cda0ec: lacks reasoning (and discussion);
18 months ago, by wenzelm
output panel: don't discard already filtered messages
18 months ago, by kleing
merged
18 months ago, by wenzelm
tuned signature: more operations;
18 months ago, by wenzelm

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 tip

isabelle