Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merged
2018-05-26, by paulson
merged
2018-05-26, by paulson
tidied some proofs
2018-05-26, by paulson
merged
2018-05-24, by paulson
merged
2018-05-24, by paulson
more small tidying
2018-05-24, by paulson
merged
2018-05-26, by Lars Hupel
macOS build: exclude HOL-Proofs
2018-05-25, by Lars Hupel
tuned;
2018-05-25, by wenzelm
merged
2018-05-25, by wenzelm
added command 'ML_export';
2018-05-25, by wenzelm
more examples;
2018-05-25, by wenzelm
tuned output;
2018-05-25, by wenzelm
pretty-print according to defaults of input syntax;
2018-05-25, by wenzelm
more accurate diagram;
2018-05-25, by wenzelm
proper output;
2018-05-25, by wenzelm
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
2018-05-24, by haftmann
merged
2018-05-24, by wenzelm
setup server directory for Cygwin quasi-mirror;
2018-05-24, by wenzelm
more scalable JVM memory management;
2018-05-24, by wenzelm
tuned output;
2018-05-24, by wenzelm
more general cache, also for term substructures;
2018-05-24, by wenzelm
more exports;
2018-05-24, by wenzelm
generalized Cramer's rule
2018-05-24, by immler
tuned
2018-05-24, by nipkow
reorganization, everything based on Tree2 now
2018-05-24, by nipkow
avoid overaggressive classical rule
2018-05-24, by haftmann
By Andrei Popescu based on an initial version by Kasper F. Brandt
2018-05-24, by nipkow
merged
2018-05-23, by paulson
small tidy-up of Complex_Transcendental
2018-05-23, by paulson
merged
2018-05-22, by paulson
small clean-up of Complex_Analysis_Basics
2018-05-21, by paulson
more complete and more correct documentation on code generation
2018-05-23, by haftmann
grouped material on numeral division
2018-05-23, by haftmann
automatic classical rule to derive a dvd b from b mod a = 0
2018-05-22, by haftmann
consider dvdE for automated classical proving
2018-05-22, by haftmann
added lambda-free HO output for Ehoh (higher-order E prototype)
2018-05-22, by blanchet
First step to remove nonstandard "[x <- xs. P]" syntax: only input
2018-05-22, by nipkow
merged
2018-05-22, by nipkow
removed unicode symbol
2018-05-22, by nipkow
Moved Landau_Symbols from the AFP to HOL-Library
2018-05-18, by Manuel Eberl
merged
2018-05-22, by wenzelm
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
2018-05-20, by wenzelm
no longer necessary
2018-05-21, by nipkow
merged
2018-05-20, by paulson
correcting the statements of the MVTs
2018-05-20, by paulson
one last fix
2018-05-20, by paulson
tidy up of Derivative
2018-05-20, by paulson
avoid undeclared frees;
2018-05-20, by wenzelm
removed junk;
2018-05-20, by wenzelm
avoid dangling tfrees;
2018-05-20, by wenzelm
standardize implicit variables: non-zero indexes do occur occasionally, e.g. via RS;
2018-05-20, by wenzelm
tuned signature;
2018-05-20, by wenzelm
avoid undeclared frees;
2018-05-20, by wenzelm
export facts;
2018-05-20, by wenzelm
clarified encoding;
2018-05-20, by wenzelm
more scalable;
2018-05-20, by wenzelm
tuned output;
2018-05-20, by wenzelm
more scalable;
2018-05-20, by wenzelm
tuned;
2018-05-20, by wenzelm
support HTTPS;
2018-05-20, by wenzelm
updated to scala-2.12.6;
2018-05-20, by wenzelm
prefer HTTPS;
2018-05-20, by wenzelm
override default of Isabelle_Process, notably for PIDE export of "document.tex";
2018-05-19, by wenzelm
tuned queries;
2018-05-19, by wenzelm
support for build_database_server (PostgreSQL);
2018-05-19, by wenzelm
clarified store.clean_output: cleanup user_output_dir even in system_mode;
2018-05-19, by wenzelm
clarified store directories;
2018-05-19, by wenzelm
tuned;
2018-05-19, by wenzelm
clarified handling of output heap;
2018-05-19, by wenzelm
tuned;
2018-05-19, by wenzelm
added lemmas
2018-05-19, by nipkow
more abstract database access;
2018-05-18, by wenzelm
tuned;
2018-05-18, by wenzelm
clarified heap vs. database operations: discontinued correlation of directory;
2018-05-18, by wenzelm
tuned;
2018-05-18, by wenzelm
tuned signature;
2018-05-18, by wenzelm
support Store with options;
2018-05-18, by wenzelm
more exports;
2018-05-18, by wenzelm
updated some Sledgehammer components, following Makarius advice
2018-05-17, by blanchet
export more theory and session structure;
2018-05-17, by wenzelm
tuned signature;
2018-05-17, by wenzelm
clarified signature;
2018-05-17, by wenzelm
read theory content from session database;
2018-05-17, by wenzelm
clarified signature;
2018-05-17, by wenzelm
misc tuning and clarification;
2018-05-17, by wenzelm
NEWS and CONTRIBUTORS for 8b50f29a1992
2018-05-17, by Andreas Lochbihler
proper PIDE positions;
2018-05-16, by wenzelm
avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
2018-05-16, by wenzelm
clarified "consolidation" vs. "presentation";
2018-05-16, by wenzelm
tuned signature;
2018-05-16, by wenzelm
merged
2018-05-16, by wenzelm
tuned;
2018-05-16, by wenzelm
more thorough checks for theory name consistency (for extend, not just merge);
2018-05-16, by wenzelm
more uniform output (cf. 450cefec7c11);
2018-05-15, by wenzelm
removed duplicates
2018-05-15, by nipkow
added lemmas
2018-05-15, by nipkow
tuned headers;
2018-05-15, by wenzelm
move FuncSet back to HOL-Library (amending 493b818e8e10)
2018-05-15, by immler
merged
2018-05-15, by nipkow
cleaning up sorted
2018-05-14, by nipkow
merged
2018-05-14, by wenzelm
support for dynamic document output while editing;
2018-05-14, by wenzelm
adjust position according to offset of command/exec id;
2018-05-14, by wenzelm
tuned signature (see Command.eval_state);
2018-05-14, by wenzelm
export generated document.tex, unless explicit document=false;
2018-05-14, by wenzelm
more general presentation hook, with document preparation as application;
2018-05-14, by wenzelm
clarified signature: more explicit type "context" with full options;
2018-05-14, by wenzelm
more explicit type Thy_Output.segment;
2018-05-14, by wenzelm
clarified signature;
2018-05-14, by wenzelm
more sorted cleaning
2018-05-14, by nipkow
cleaning up sorted
2018-05-14, by nipkow
merged
2018-05-13, by wenzelm
more uniform types vs. consts;
2018-05-13, by wenzelm
more concise information;
2018-05-13, by wenzelm
export foundational theory content in Scala;
2018-05-13, by wenzelm
clarified markup;
2018-05-13, by wenzelm
tuned signature;
2018-05-13, by wenzelm
tuned -- use XZ.Cache;
2018-05-13, by wenzelm
clarified implicit compression;
2018-05-13, by wenzelm
tuned -- use XZ.Cache;
2018-05-13, by wenzelm
more exports;
2018-05-13, by wenzelm
tuned;
2018-05-13, by wenzelm
more operations;
2018-05-13, by wenzelm
tuned
2018-05-13, by nipkow
tuned
2018-05-13, by nipkow
mv lemma
2018-05-13, by nipkow
removed unused lemma
2018-05-13, by nipkow
tuned
2018-05-13, by nipkow
removed some non-essential rules
2018-05-12, by haftmann
added lemmas
2018-05-12, by nipkow
new tool Code_Lazy
2018-05-12, by Andreas Lochbihler
some export of foundational theory content;
2018-05-11, by wenzelm
support for general theory presentation;
2018-05-11, by wenzelm
guard result exports via export_pattern -- avoid bombing client via huge blobs;
2018-05-11, by wenzelm
tuned;
2018-05-11, by wenzelm
clarified output: avoid costly operations on huge blobs;
2018-05-11, by wenzelm
unused;
2018-05-11, by wenzelm
more scalable -- avoid huge lines within stdout;
2018-05-11, by wenzelm
slightly more ambitious parallelism (again);
2018-05-11, by wenzelm
more scalable API;
2018-05-11, by wenzelm
proper heading;
2018-05-11, by wenzelm
removed unused Java FX modules (it will be unbundled from JDK eventually);
2018-05-11, by wenzelm
tidied some messy proofs
2018-05-10, by paulson
merged
2018-05-10, by nipkow
more lemmas
2018-05-10, by nipkow
merged
2018-05-10, by nipkow
simpler types
2018-05-10, by nipkow
auto-tidying
2018-05-10, by paulson
merged
2018-05-10, by paulson
more on infinite products
2018-05-10, by paulson
merged
2018-05-09, by paulson
part tidy-up of Determinants
2018-05-09, by paulson
less ambitious parallelism, notably for threads=2;
2018-05-09, by wenzelm
more informative error, notably for missing executable;
2018-05-09, by wenzelm
tuned signature;
2018-05-09, by wenzelm
clarified future scheduling parameters, with support for parallel_limit;
2018-05-09, by wenzelm
record total number of tasks;
2018-05-09, by wenzelm
merged
2018-05-09, by paulson
more infinite product theorems
2018-05-09, by paulson
proper merge of items without term index (amending b969263fcf02);
2018-05-09, by wenzelm
announce sorted changes
2018-05-09, by nipkow
merged
2018-05-08, by paulson
one tiny fix
2018-05-08, by paulson
merged
2018-05-08, by paulson
merged
2018-05-08, by paulson
tidying more messy proofs
2018-05-08, by paulson
merged
2018-05-08, by nipkow
more efficient code
2018-05-08, by nipkow
merged
2018-05-08, by wenzelm
command-line tool "isabelle export";
2018-05-08, by wenzelm
more efficient query;
2018-05-08, by wenzelm
more robust: self-export only;
2018-05-08, by wenzelm
tuned signature;
2018-05-08, by wenzelm
merged
2018-05-08, by nipkow
more "sorted" changes
2018-05-08, by nipkow
more "sorted" changes
2018-05-08, by nipkow
new def of sorted and sorted_wrt
2018-05-08, by nipkow
more operations;
2018-05-07, by wenzelm
merged
2018-05-07, by wenzelm
return exports as result for Isabelle server;
2018-05-07, by wenzelm
more checks;
2018-05-07, by wenzelm
tuned;
2018-05-07, by wenzelm
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
2018-05-07, by wenzelm
clarified signature;
2018-05-07, by wenzelm
store exports within PIDE command state;
2018-05-07, by wenzelm
removed some lemma duplicates
2018-05-06, by haftmann
typo
2018-05-06, by haftmann
more appropriate notion of emptiness
2018-05-06, by haftmann
merged
2018-05-06, by paulson
more tidying
2018-05-06, by paulson
starting to tidy up Interval_Integral.thy
2018-05-06, by paulson
more operations;
2018-05-06, by wenzelm
merged
2018-05-06, by wenzelm
store exports in session database, with asynchronous / parallel compression;
2018-05-06, by wenzelm
tuned signature;
2018-05-06, by wenzelm
tuned signature;
2018-05-06, by wenzelm
tuned signature;
2018-05-06, by wenzelm
protocol message for export of theory resources;
2018-05-05, by wenzelm
hexadecimal representation of byte string;
2018-05-05, by wenzelm
cleanup session output before starting build job;
2018-05-05, by wenzelm
reinstated old lemma name
2018-05-06, by nipkow
updated to lemma name change
2018-05-06, by nipkow
removed asm "finite"
2018-05-06, by nipkow
merged
2018-05-04, by wenzelm
no censorship of view title;
2018-05-04, by wenzelm
set view title dynamically;
2018-05-04, by wenzelm
tuned
2018-05-04, by nipkow
tuned
2018-05-04, by nipkow
Some tidying up (mostly regarding summations from 0)
2018-05-03, by paulson
tidied up Infinite_Products
2018-05-03, by paulson
merged
2018-05-03, by immler
fixed HOL-Analysis
2018-05-03, by immler
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
2018-05-03, by immler
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
2018-05-02, by immler
a lemma about infinite products
2018-05-03, by paulson
merged
2018-05-02, by paulson
tidying up and using real induction methods
2018-05-02, by paulson
tuned -- slightly smaller future closure size;
2018-05-02, by wenzelm
clarified menu actions;
2018-05-02, by wenzelm
purge history more thoroughly (see also 3156faac30a7);
2018-05-02, by wenzelm
merged
2018-05-02, by paulson
type class generalisations; some work on infinite products
2018-05-02, by paulson
merged
2018-05-02, by paulson
simplified some messy proofs
2018-05-01, by paulson
clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations);
2018-05-01, by wenzelm
avoid output showing up in kill ring (via TextArea.setText, JEditBuffer.remove, UndoManager.contentRemoved), e.g. relevant for action "paste-deleted";
2018-05-01, by wenzelm
merged
2018-04-30, by paulson
more general tidying up
2018-04-30, by paulson
prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas
2018-04-30, by boehmes
cleaned up more messy proofs
2018-04-29, by paulson
more defer/prefer
2018-04-29, by paulson
getting rid of more "defer", etc.
2018-04-28, by paulson
getting rid of "defer"
2018-04-28, by paulson
another big cleanup
2018-04-27, by paulson
merged
2018-04-27, by paulson
minor typeclass generalisations and junk removal
2018-04-27, by paulson
merged
2018-04-26, by paulson
more messy proofs
2018-04-26, by paulson
merged
2018-04-26, by nipkow
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip