isabelle: Graph

New material in support of quaternions
2018-06-18, by paulson
De-applied Ideal.thy
2018-06-18, by paulson
material on finite sets and maps
2018-06-18, by Lars Hupel
simplify parametricity proofs
2018-06-18, by Lars Hupel
merged
2018-06-18, by nipkow
added simp rules
2018-06-17, by nipkow
merged
2018-06-17, by paulson
Algebra tidy-up
2018-06-17, by paulson
added simp rule
2018-06-17, by nipkow
more simp
2018-06-16, by nipkow
moved lemmas from AFP
2018-06-16, by nipkow
moved lemmas from AFP
2018-06-16, by nipkow
merged
2018-06-15, by paulson
more on infinite products. Also subgroup_imp_subset -> subgroup.subset
2018-06-15, by paulson
empty -> Map.empty
2018-06-15, by nipkow
Map.empty now qualified to avoid name clashes
2018-06-15, by nipkow
auto update;
2018-06-14, by wenzelm
merged
2018-06-14, by paulson
Adjusting Number_Theory for new Algebra
2018-06-14, by paulson
merged
2018-06-14, by paulson
reorganisation of Algebra: new material from Baillon and Vilhena, removal of duplicate names, elimination of "More_" theories
2018-06-14, by paulson
merged
2018-06-12, by paulson
New material from Martin Baillon and Paulo Emílio de Vilhena
2018-06-12, by paulson
tuned
2018-06-14, by nipkow
removed duplicates
2018-06-14, by nipkow
qualify interpretations to avoid clashes
2018-06-13, by nipkow
more abstract names
2018-06-13, by nipkow
tuned exception
2018-06-13, by immler
restructured
2018-06-13, by immler
result of unoverload is not in normal form
2018-06-13, by immler
tuned
2018-06-13, by immler
allow for a list of vars
2018-06-13, by immler
parse var
2018-06-13, by immler
merged
2018-06-12, by nipkow
more abstract naming
2018-06-12, by nipkow
tuned
2018-06-12, by immler
workaround: in internalize_sort, Thm.unconstrainT can rename type variables and therefore invalidate new_tvar
2018-06-12, by immler
a derived rule combining unoverload and internalize_sort
2018-06-12, by immler
merged
2018-06-12, by paulson
fixed a name clash
2018-06-11, by paulson
merged
2018-06-11, by paulson
the last of the infinite product proofs
2018-06-11, by paulson
merged
2018-06-12, by nipkow
proved avl for map (finally); tuned
2018-06-12, by nipkow
merged
2018-06-11, by paulson
tidier Cauchy proofs
2018-06-11, by paulson
merged
2018-06-11, by wenzelm
more abstract Export.Provider;
2018-06-11, by wenzelm
clarified signature: persistent results;
2018-06-11, by wenzelm
tuned signature;
2018-06-11, by wenzelm
tuned def. of del and proved preservation of rbt (finally)
2018-06-11, by nipkow
merged
2018-06-11, by nipkow
tuned order of arguments
2018-06-11, by nipkow
default value for parametricity of dim
2018-06-11, by immler
added lemma
2018-06-11, by nipkow
clarified signature: more uniform theory_message (see also d7920eb7de54);
2018-06-09, by wenzelm
tuned -- use existing operation;
2018-06-09, by wenzelm
merged
2018-06-07, by wenzelm
isabelle emacs no longer exists;
2018-06-07, by wenzelm
utilize 'flip'
2018-06-07, by nipkow
comments
2018-06-07, by nipkow
merged
2018-06-06, by nipkow
reorient -> split; documented split
2018-06-06, by nipkow
merged
2018-06-06, by wenzelm
Added tag Isabelle2018-RC0 for changeset 194fa3d2d6a4
2018-06-06, by wenzelm
merged
2018-06-06, by paulson
resolution of name clashes in Algebra
2018-06-06, by paulson
merged
2018-06-06, by wenzelm
isabelle update_comments;
2018-06-06, by wenzelm
tuned header;
2018-06-06, by wenzelm
updated for release;
2018-06-06, by wenzelm
updated for release;
2018-06-06, by wenzelm
misc tuning and updates for release;
2018-06-06, by wenzelm
updated for release;
2018-06-06, by wenzelm
updated for release;
2018-06-06, by wenzelm
eliminated suspicious Unicode;
2018-06-06, by wenzelm
proper white space;
2018-06-06, by wenzelm
updated to sqlite-jdbc-3.23.1;
2018-06-06, by wenzelm
merged
2018-06-06, by nipkow
Keep filter input syntax
2018-06-06, by nipkow
more parallelism to cope with 8h30 CPU time;
2018-06-05, by wenzelm
full benchmarks, including all conditional theories;
2018-06-05, by wenzelm
tuned proofs;
2018-06-05, by wenzelm
more robust;
2018-06-05, by wenzelm
less wasteful consolidation, based on PIDE front-end state and recent changes;
2018-06-05, by wenzelm
tuned -- short-circuit result;
2018-06-05, by wenzelm
tuned;
2018-06-05, by wenzelm
updated URLs;
2018-06-05, by wenzelm
merged
2018-06-04, by wenzelm
more robust;
2018-06-04, by wenzelm
avoid hardwired cygwin mirror;
2018-06-04, by wenzelm
updated to current Cygwin, after 2.10.0-1 from 02-Feb-2018;
2018-06-04, by wenzelm
NEWS: infinite products
2018-06-04, by paulson
merged
2018-06-04, by paulson
more tweaks of Cauchy
2018-06-04, by paulson
clarified signature;
2018-06-04, by wenzelm
tuned proofs;
2018-06-03, by wenzelm
NEWS;
2018-06-03, by wenzelm
proper function invocation with all arguments;
2018-06-03, by wenzelm
fork parallel prints early in execution: avoid degradation of priority due to main eval task;
2018-06-03, by wenzelm
clarified signature: prefer Document.Snapshot;
2018-06-03, by wenzelm
list syntax details
2018-06-03, by nipkow
merged
2018-06-03, by nipkow
allow tuple patterns in list comprehensions
2018-06-03, by nipkow
infinite product material
2018-06-03, by paulson
merged
2018-06-02, by paulson
tidied more Cauchy proofs
2018-06-02, by paulson
tuned proofs;
2018-06-02, by wenzelm
more symbols;
2018-06-02, by wenzelm
more formal comments;
2018-06-02, by wenzelm
more args;
2018-06-02, by wenzelm
record active execution task and depend on it -- avoid new executions bumping into old ones;
2018-06-02, by wenzelm
tuned -- more explicit types;
2018-06-02, by wenzelm
less frequent consolidation: it requires a full Document.update and Document.start_execution;
2018-06-02, by wenzelm
varify frees, notably dangling_params (see also e0cd57aeb60c);
2018-06-01, by wenzelm
tuned -- more explicit expression;
2018-06-01, by wenzelm
merged
2018-06-01, by wenzelm
documentation for "isabelle dump";
2018-06-01, by wenzelm
more dump aspects, with options;
2018-06-01, by wenzelm
tuned signature;
2018-06-01, by wenzelm
clarified default: all aspects;
2018-06-01, by wenzelm
clarified priority;
2018-06-01, by wenzelm
merged
2018-06-01, by nipkow
added lemma
2018-06-01, by nipkow
Fixed latex markup
2018-06-01, by paulson
merged
2018-06-01, by paulson
more tidying
2018-06-01, by paulson
merged
2018-05-31, by wenzelm
more symbols;
2018-05-31, by wenzelm
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
2018-05-31, by wenzelm
clarified: consolidated result is last command;
2018-05-31, by wenzelm
support for anonymous print function values;
2018-05-31, by wenzelm
tuned;
2018-05-30, by wenzelm
store Isabelle symbols in canonical form;
2018-05-30, by wenzelm
clarified outermost progress.interrupt_handler;
2018-05-30, by wenzelm
report theory progress via PIDE node status;
2018-05-30, by wenzelm
merge
2018-05-31, by blanchet
more conservative output, avoiding nonstandard feature of E
2018-05-31, by blanchet
merged
2018-05-30, by paulson
winding numbers predicate
2018-05-30, by paulson
unused
2018-05-30, by nipkow
merged
2018-05-29, by wenzelm
more node status information;
2018-05-29, by wenzelm
tuned signature;
2018-05-29, by wenzelm
tuned signature;
2018-05-29, by wenzelm
shutdown ML process before output: Theories_Result is timeless/stateless;
2018-05-29, by wenzelm
more operations;
2018-05-29, by wenzelm
more accurate dependencies;
2018-05-29, by wenzelm
tuned;
2018-05-29, by wenzelm
more formal dump aspects;
2018-05-29, by wenzelm
more operations (as in ML);
2018-05-29, by wenzelm
clarified option -O: avoid conflict with build/dump option -D;
2018-05-29, by wenzelm
slicker proof
2018-05-29, by nipkow
canonical names
2018-05-29, by nipkow
merged
2018-05-28, by paulson
more general tidying
2018-05-28, by paulson
merged
2018-05-28, by wenzelm
support to dump build database produced by PIDE session;
2018-05-28, by wenzelm
more accurate theory_graph: avoid imports of loaded_theories with incomplete node name;
2018-05-28, by wenzelm
clarified signature: Known.theories retains Document.Node.Entry (with header);
2018-05-28, by wenzelm
clarified signature;
2018-05-28, by wenzelm
tuned signature;
2018-05-28, by wenzelm
merged
2018-05-27, by paulson
tidying up a bit more
2018-05-27, by paulson
prefer existing operation;
2018-05-27, by wenzelm
retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;
2018-05-27, by wenzelm
clarified signature -- avoid confusion with Resources.is_hidden;
2018-05-27, by wenzelm
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
2018-05-27, by wenzelm
merged
2018-05-26, by paulson
tidying and reorganisation around Cauchy Integral Theorem
2018-05-26, by paulson
export sort algebra;
2018-05-26, by wenzelm
tuned;
2018-05-26, by wenzelm
tuned;
2018-05-26, by wenzelm
support 'export_files' in session ROOT;
2018-05-26, by wenzelm
clarified output;
2018-05-26, by wenzelm
support multiple patterns;
2018-05-26, by wenzelm
clarified cache;
2018-05-26, by wenzelm
tuned signature;
2018-05-26, by wenzelm
tuned output;
2018-05-26, by wenzelm
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