Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+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
2016-08-17, by traytel
coinduction method accepts a list of coinduction rules (takes the first matching one)
2016-03-04, by traytel
more robust;
2016-08-16, by wenzelm
clarified presentation order, according to typical amounts;
2016-08-16, by wenzelm
present ML timing as well;
2016-08-16, by wenzelm
Polynomial algebra cleanup (tuned)
2016-08-16, by eberlm
Polynomial algebra cleanup
2016-08-16, by eberlm
provide index.html;
2016-08-14, by wenzelm
cpu time is optional (see Timing.message_resources);
2016-08-14, by wenzelm
proper display of "_";
2016-08-14, by wenzelm
clarified options and arguments;
2016-08-14, by wenzelm
updated NEWS
2016-08-14, by blanchet
optimized parent computation in MaSh
2016-08-14, by blanchet
avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
2016-08-14, by blanchet
tuned MaSh's metacharacters to avoid needless decoding
2016-08-14, by blanchet
optimization in MaSh parsing
2016-08-14, by blanchet
tuned ML
2016-08-14, by blanchet
removed trailing final stops in Nitpick messages
2016-08-14, by blanchet
killed final stops in Sledgehammer and friends
2016-08-14, by blanchet
tuned message
2016-08-14, by blanchet
tuning punctuation in messages output by Isabelle
2016-08-14, by blanchet
tuning whitespace in output syntax
2016-08-14, by blanchet
gnuplot presentation similar to former isatest-statistics;
2016-08-13, by wenzelm
tuned;
2016-08-13, by wenzelm
statistics from session build output;
2016-08-13, by wenzelm
more uniform output;
2016-08-13, by wenzelm
added [simp] lemmas
2016-08-13, by nipkow
more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;
2016-08-12, by wenzelm
merged
2016-08-12, by wenzelm
active jEdit actions;
2016-08-12, by wenzelm
more symbols;
2016-08-12, by wenzelm
clarified syntax;
2016-08-12, by wenzelm
updated;
2016-08-12, by wenzelm
some icons from Symbola font;
2016-08-12, by wenzelm
more latex symbols, notably for embedded ML;
2016-08-12, by wenzelm
uniform ML and document antiquotations;
2016-08-12, by wenzelm
proper completion of path cartouche (amending 5a7c919a4ada);
2016-08-12, by wenzelm
clarified error;
2016-08-12, by wenzelm
more uniform path syntax (like url);
2016-08-12, by wenzelm
liberal name as in document antiquotations;
2016-08-12, by wenzelm
tuned;
2016-08-12, by wenzelm
clarified antiquotations;
2016-08-11, by wenzelm
tuned error;
2016-08-11, by wenzelm
tuned whitespace;
2016-08-11, by wenzelm
suppress ASCII art;
2016-08-11, by wenzelm
added lemma
2016-08-12, by nipkow
tuned
2016-08-12, by nipkow
Extracted floorlog and bitlen to separate theory Log_Nat
2016-08-12, by nipkow
lists form a monoid
2016-08-10, by haftmann
formal passive interpretation proofs for conj and disj
2016-08-10, by haftmann
add monotonicity propertyies of `mult1` and `mult`
2016-08-08, by Bertram Felgenhauer
keeping lifting rules local
2016-08-10, by haftmann
epheremal interpretation keeps auxiliary definition localized
2016-08-10, by haftmann
tuned order of declarations and proofs
2016-08-10, by haftmann
tuned
2016-08-11, by nipkow
simplified theory hierarchy;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
misc tuning and modernization;
2016-08-10, by wenzelm
merged
2016-08-10, by nipkow
"split add" -> "split".
2016-08-10, by nipkow
tuned proofs;
2016-08-10, by wenzelm
"split add" -> "split"
2016-08-10, by nipkow
merged
2016-08-09, by wenzelm
API for Isabelle Jenkins continuous integration services;
2016-08-09, by wenzelm
more operations;
2016-08-09, by wenzelm
support for JSON parsing;
2016-08-09, by wenzelm
New theory Balance_List
2016-08-09, by nipkow
more operations;
2016-08-09, by wenzelm
merged;
2016-08-09, by wenzelm
print name in parsable form;
2016-08-09, by wenzelm
clarified bootstrap;
2016-08-09, by wenzelm
merged
2016-08-09, by nipkow
adapted ZF,FOL,CCL,LCF to modified splitter
2016-08-09, by nipkow
introduced aggressive splitter "split!"
2016-08-09, by nipkow
Tuned primes
2016-08-09, by eberlm
Merged
2016-08-09, by eberlm
is_prime -> prime
2016-08-08, by eberlm
Item_Net.retrieve_matching requires beta-eta normal form (amending 8976c5bc9e97);
2016-08-08, by wenzelm
merged
2016-08-08, by wenzelm
tuned proof;
2016-08-08, by wenzelm
tuned;
2016-08-08, by wenzelm
tuned;
2016-08-08, by wenzelm
rename HOL-Multivariate_Analysis to HOL-Analysis.
2016-08-08, by hoelzl
move measure theory from HOL-Probability to HOL-Multivariate_Analysis
2016-08-05, by hoelzl
misc tuning and modernization;
2016-08-07, by wenzelm
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
2016-08-06, by wenzelm
tuned signature;
2016-08-06, by wenzelm
some additions to FSet
2016-08-06, by Lars Hupel
tuned
2016-08-06, by nipkow
clarified Sidekick setup;
2016-08-05, by wenzelm
more tight filtering;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
clarified -- more standard maxidx;
2016-08-05, by wenzelm
tuned -- maxidx unused;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
tuned;
2016-08-05, by wenzelm
merged
2016-08-05, by wenzelm
misc tuning and modernization;
2016-08-05, by wenzelm
tuned whitespace;
2016-08-05, by wenzelm
Sidekick parser for isabelle-ml and sml mode;
2016-08-05, by wenzelm
prefer hardwired "nothing";
2016-08-04, by wenzelm
NEWS;
2016-08-04, by wenzelm
clarified handling of plain theory commands;
2016-08-04, by wenzelm
support for context block structure in Sidekick;
2016-08-04, by wenzelm
tuned;
2016-08-04, by wenzelm
clarified modules;
2016-08-04, by wenzelm
clarified modules;
2016-08-04, by wenzelm
merged
2016-08-05, by nipkow
added missing lemmas
2016-08-05, by nipkow
fixed floor proof
2016-08-05, by nipkow
fixed floor proofs
2016-08-05, by nipkow
added min_height
2016-08-05, by nipkow
tuned floor lemmas
2016-08-05, by nipkow
more lemmas
2016-08-05, by nipkow
clean up prove for inter_interior_unions_intervals
2016-08-05, by hoelzl
HOL-Multivariate_Analysis: rename theories for more descriptive names
2016-08-04, by hoelzl
HOL-Multivariate_Analysis: replace neutral, monoidal, and iterate by the comm_monoid_set versions. Changed operative to comm_monoid_set. Renamed support_on to support and changed to comm_monoid_add.
2016-08-04, by hoelzl
include 'begin' and 'end' structure in text folds;
2016-08-03, by wenzelm
tuned proof;
2016-08-02, by wenzelm
proper latex rendering of abbrevs templates (e.g. src/HOL/Nonstandard_Analysis/HLim.thy);
2016-08-02, by wenzelm
more symbols;
2016-08-02, by wenzelm
misc tuning and modernization;
2016-08-02, by wenzelm
implicit keyword completion only for actual words (amending 73939a9b70a3);
2016-08-02, by wenzelm
merged
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
tuned signature -- prover-independence is presently theoretical;
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
avoid confusion with 'case' and "cases";
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
clarified: 'imports' is de-facto mandatory;
2016-08-02, by wenzelm
support 'abbrevs' within theory header;
2016-08-02, by wenzelm
tuned;
2016-08-02, by wenzelm
more natural definition of type finmap
2016-08-02, by immler
tuned proof;
2016-08-01, by wenzelm
misc tuning and modernization;
2016-08-01, by wenzelm
uniform server startup like windows and macos, for improved robustness if jEdit is terminated abruptly;
2016-08-01, by wenzelm
more restrictive retrieval of rules for matching instead of unification -- relevant for performance of printing terms;
2016-08-01, by wenzelm
misc tuning and modernization;
2016-07-31, by wenzelm
clarified imports;
2016-07-31, by wenzelm
simplified theory structure;
2016-07-31, by wenzelm
misc tuning and modernization;
2016-07-31, by wenzelm
tuned;
2016-07-30, by wenzelm
merged
2016-07-29, by wenzelm
more accurate cong del;
2016-07-29, by wenzelm
made generation of transfer goals more robust w.r.t. dead variables
2016-07-29, by traytel
merged
2016-07-29, by Andreas Lochbihler
prefer [simp] over [iff] as [iff] break HOL-UNITY
2016-07-29, by Andreas Lochbihler
fix LaTeX error
2016-07-29, by Andreas Lochbihler
add lemmas contributed by Peter Gammie
2016-07-29, by Andreas Lochbihler
more instantiations for multiset
2016-07-29, by fleury
merged
2016-07-28, by wenzelm
misc tuning and modernization;
2016-07-28, by wenzelm
updated to jdk-8u102;
2016-07-27, by wenzelm
numerical bounds on pi
2016-07-28, by immler
more on type class hierarchy
2016-07-24, by haftmann
simplified
2016-07-24, by haftmann
text antiquotation for locales (similar to classes)
2016-07-24, by haftmann
NEWS: Primes
2016-07-27, by Manuel Eberl
honor sorts in (co)datatype declarations
2016-07-26, by traytel
misc tuning and modernization;
2016-07-26, by wenzelm
more symbols;
2016-07-25, by wenzelm
unused (see 1e9e68247ad1);
2016-07-25, by wenzelm
merged
2016-07-25, by wenzelm
misc tuning and modernization;
2016-07-22, by wenzelm
misc tuning and modernization;
2016-07-22, by wenzelm
clarified def vs. ref focus, e.g. for calculation vs. command refs;
2016-07-22, by wenzelm
entity markup for calculation;
2016-07-22, by wenzelm
tuned;
2016-07-22, by wenzelm
more markup for unstructured calculation;
2016-07-22, by wenzelm
tuned proofs -- avoid unstructured calculation;
2016-07-22, by wenzelm
tuned proofs -- avoid improper use of "this";
2016-07-22, by wenzelm
added new vcg based on existentially quantified while-rule
2016-07-23, by nipkow
Removed redundant material related to primes
2016-07-22, by eberlm
Merged
2016-07-22, by eberlm
Tuned primes
2016-07-22, by eberlm
Overhaul of prime/multiplicity/prime_factors
2016-07-21, by eberlm
merged
2016-07-21, by wenzelm
provide Pure.simp/simp_all, which only know about meta-equality;
2016-07-20, by wenzelm
clarified imports;
2016-07-20, by wenzelm
tuned;
2016-07-20, by wenzelm
oops;
2016-07-20, by wenzelm
completion templates for commands involving "begin ... end" blocks;
2016-07-20, by wenzelm
moved method "use" to Pure;
2016-07-20, by wenzelm
unused (see also 651ea265d568);
2016-07-20, by wenzelm
more instantiations for multiset
2016-07-20, by fleury
adding mset_map to the simp rules
2016-07-20, by fleury
misc tuning and simplification;
2016-07-19, by wenzelm
misc tuning and simplification;
2016-07-19, by wenzelm
added missing transfer rule
2016-07-19, by Lars Hupel
Linux platform base-line is Ubuntu 12.04 LTS;
2016-07-19, by wenzelm
more precise error information for dynamic Scala tools
2016-07-17, by Lars Hupel
tuned signature;
2016-07-16, by wenzelm
no Output.information by default, e.g. "isabelle console", "isabelle build";
2016-07-16, by wenzelm
tuned proofs;
2016-07-16, by wenzelm
re-use name space serial as unique (!) id;
2016-07-16, by wenzelm
clarified;
2016-07-16, by wenzelm
information about proof outline with cases (sendback);
2016-07-16, by wenzelm
tuned signature;
2016-07-16, by wenzelm
more operations;
2016-07-15, by wenzelm
singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
2016-07-15, by wenzelm
unused;
2016-07-15, by wenzelm
more structured edit, including indentation;
2016-07-15, by wenzelm
clarified markup;
2016-07-15, by wenzelm
merged
2016-07-15, by wenzelm
misc tuning and modernization;
2016-07-15, by wenzelm
Merged
2016-07-15, by eberlm
Tuned Gcd/Lcm in Codegenerator_Test
2016-07-15, by eberlm
Merged
2016-07-15, by eberlm
Tuned Bool_List_Representation
2016-07-15, by eberlm
Added normalized fractions
2016-07-14, by eberlm
Tuned looping simp rules in semiring_div
2016-07-14, by eberlm
Reformed factorial rings
2016-07-13, by eberlm
HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
2016-07-15, by hoelzl
merged
2016-07-15, by wenzelm
proper latex;
2016-07-15, by wenzelm
misc tuning and modernization;
2016-07-15, by wenzelm
Got rid of the \nexists macro
2016-07-14, by paulson
More advanced theorems about retracts, homotopies., etc
2016-07-14, by paulson
prefer HTTPS;
2016-07-14, by wenzelm
prefer curl: presumably more portable and versatile;
2016-07-14, by wenzelm
misc tuning and modernization;
2016-07-14, by wenzelm
merged
2016-07-13, by wenzelm
misc tuning and modernization;
2016-07-13, by wenzelm
merged
2016-07-13, by wenzelm
misc tuning and modernization;
2016-07-13, by wenzelm
auto indentation of quasi commands;
2016-07-13, by wenzelm
tuned;
2016-07-13, by wenzelm
clarified indentation (amending 37a3fc20154d);
2016-07-13, by wenzelm
tuned;
2016-07-13, by wenzelm
tuned;
2016-07-13, by wenzelm
tuned;
2016-07-13, by wenzelm
clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal;
2016-07-13, by wenzelm
clarified indentation: 'begin' is treated like a separate command without indent;
2016-07-13, by wenzelm
tuned;
2016-07-13, by wenzelm
obsolete;
2016-07-13, by wenzelm
semantic indentation for unstructured proof scripts;
2016-07-13, by wenzelm
misc tuning and modernization;
2016-07-13, by wenzelm
tuned
2016-07-13, by Lars Hupel
remove obsolete isatest scripts
2016-07-13, by Lars Hupel
Merge
2016-07-13, by paulson
lots of new theorems about differentiable_on, retracts, ANRs, etc.
2016-07-13, by paulson
tuning
2016-07-13, by blanchet
misc tuning and modernization;
2016-07-12, by wenzelm
misc tuning and modernization;
2016-07-12, by wenzelm
misc tuning and modernization;
2016-07-12, by wenzelm
more standard name;
2016-07-12, by wenzelm
merged
2016-07-12, by wenzelm
misc tuning and modernization;
2016-07-12, by wenzelm
NEWS;
2016-07-12, by wenzelm
clarified;
2016-07-12, by wenzelm
clarified;
2016-07-12, by wenzelm
closing 'qed' or '}' is outside of fold;
2016-07-12, by wenzelm
tuned;
2016-07-12, by wenzelm
sharing simp rules between ordered monoids and rings
2016-07-12, by fleury
added action "isabelle.newline" (shortcut ENTER);
2016-07-12, by wenzelm
tuned signature;
2016-07-12, by wenzelm
merged
2016-07-11, by wenzelm
NEWS;
2016-07-11, by wenzelm
clarified indentation;
2016-07-11, by wenzelm
indentation of brackets;
2016-07-11, by wenzelm
clarified keywords;
2016-07-11, by wenzelm
clarified keywords;
2016-07-11, by wenzelm
proper filter;
2016-07-11, by wenzelm
tunes signature;
2016-07-11, by wenzelm
observe comments in indentation, but not in fold structure;
2016-07-11, by wenzelm
support more modes;
2016-07-11, by wenzelm
clarified keywords;
2016-07-11, by wenzelm
clarified indentation;
2016-07-11, by wenzelm
explicit kind "before_command";
2016-07-11, by wenzelm
clarified indentation involving 'begin';
2016-07-11, by wenzelm
more robust;
2016-07-11, by wenzelm
NEWS
2016-07-11, by haftmann
restored executability of cmp
2016-07-11, by nipkow
merged
2016-07-11, by wenzelm
clarified keywords;
2016-07-11, by wenzelm
more indentation for quasi_command keywords;
2016-07-11, by wenzelm
tuned;
2016-07-11, by wenzelm
tuned;
2016-07-11, by wenzelm
tuned;
2016-07-11, by wenzelm
support for quasi_command keywords;
2016-07-10, by wenzelm
tuned signature: more uniform Keyword.spec;
2016-07-10, by wenzelm
indentation in reminiscence to Proof General (see proof-indent.el);
2016-07-08, by wenzelm
tuned;
2016-07-08, by wenzelm
tuned;
2016-07-08, by wenzelm
tuned;
2016-07-07, by wenzelm
clarified signature;
2016-07-07, by wenzelm
more operations;
2016-07-07, by wenzelm
clarified modules;
2016-07-07, by wenzelm
basic setup for indentation;
2016-07-07, by wenzelm
tuned;
2016-07-07, by wenzelm
more operations;
2016-07-07, by wenzelm
tuned
2016-07-10, by Lars Hupel
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
2016-07-09, by haftmann
avoid to hide equality behind (output) abbreviation
2016-07-08, by haftmann
default rule for single-step reasoning
2016-07-08, by haftmann
new style dummy_pats
2016-07-08, by nipkow
added path_len
2016-07-08, by nipkow
merged
2016-07-07, by nipkow
got rid of class cmp; added height-size proofs by Daniel Stuewe
2016-07-07, by nipkow
more instantiations for multiset
2016-07-07, by fleury
moved lemmas and locales around (with minor incompatibilities)
2016-07-07, by blanchet
updated example
2016-07-07, by blanchet
leverage new 'order' type class instantiation in multiset
2016-07-06, by blanchet
updated examples
2016-07-06, by blanchet
merged
2016-07-06, by wenzelm
misc tuning and modernization;
2016-07-06, by wenzelm
proper signature;
2016-07-06, by wenzelm
tuned signature;
2016-07-06, by wenzelm
simplify build scripts
2016-07-06, by Lars Hupel
misc tuning and modernization;
2016-07-05, by wenzelm
more antiquotations;
2016-07-05, by wenzelm
tuned;
2016-07-05, by wenzelm
merged
2016-07-05, by wenzelm
PIDE reports of implicit variable scope;
2016-07-05, by wenzelm
PIDE reports of implicit variable scope;
2016-07-05, by wenzelm
tuned;
2016-07-05, by wenzelm
Probability: simplified Levy's uniqueness theorem
2016-07-05, by hoelzl
avoid reference to invisible theorem, by using another one instead (suggested by Anders Schlichtkrull; the document's author is incomunicado)
2016-07-05, by blanchet
tuning
2016-07-05, by blanchet
typo (reported by Anders Schlichtkrull)
2016-07-05, by blanchet
simplified proof for measurability of isCont
2016-07-05, by hoelzl
instantiate multiset with multiset ordering
2016-07-05, by fleury
more accurate total timing
2016-07-05, by Lars Hupel
merged
2016-07-05, by Lars Hupel
tuned
2016-07-04, by Lars Hupel
merged
2016-07-04, by wenzelm
NEWS;
2016-07-04, by wenzelm
clarified positions, e.g. for reports on literal facts;
2016-07-04, by wenzelm
tuned whitespace;
2016-07-04, by wenzelm
tuned;
2016-07-04, by wenzelm
tuned;
2016-07-04, by wenzelm
spelling
2016-07-04, by haftmann
combinator to build partial equivalence relations from a predicate and an equivalenc relation
2016-07-04, by haftmann
default one-step rules for predicates on relations;
2016-07-04, by haftmann
basic facts about almost everywhere fix bijections
2016-07-04, by haftmann
dedicated locale for total bijections
2016-07-04, by haftmann
tuned sections
2016-07-04, by haftmann
relating gbinomial and binomial, still using distinct definitions
2016-07-04, by haftmann
clarified fact position, notably for reports on literal facts;
2016-07-04, by wenzelm
more accurate facts index;
2016-07-04, by wenzelm
tuned signature;
2016-07-04, by wenzelm
tuned signature;
2016-07-04, by wenzelm
simplified definitions of combinatorial functions
2016-07-02, by haftmann
define binomial coefficents directly via combinatorial definition
2016-07-02, by haftmann
more theorems
2016-07-02, by haftmann
abstract and concrete multiplicative groups
2016-07-02, by haftmann
more correct comment
2016-07-02, by haftmann
clarified;
2016-07-01, by wenzelm
misc tuning and modernization;
2016-07-01, by wenzelm
Tuned multiset lattice
2016-07-01, by Manuel Eberl
More lemmas on Gcd/Lcm
2016-07-01, by Manuel Eberl
Conditionally complete lattice of multisets
2016-07-01, by Manuel Eberl
added fundef_cong rule
2016-06-26, by nipkow
misc tuning and modernization;
2016-06-24, by wenzelm
misc tuning and modernization;
2016-06-24, by wenzelm
merged
2016-06-23, by wenzelm
misc tuning and modernization;
2016-06-23, by wenzelm
tuned signature;
2016-06-23, by wenzelm
avoid overlapping equations for gcd, lcm on integers
2016-06-23, by haftmann
compiling implicit instances into companion objects for classes avoids ambiguities
2016-06-23, by haftmann
print statistics; tuned
2016-06-22, by Lars Hupel
adjust job/thread count for new hardware
2016-06-22, by Lars Hupel
report class parameters within instantiation;
2016-06-22, by wenzelm
clarified PIDE markup;
2016-06-22, by wenzelm
tuned;
2016-06-22, by wenzelm
tuned signature;
2016-06-22, by wenzelm
bundle lifting_syntax;
2016-06-22, by wenzelm
tuned;
2016-06-21, by wenzelm
clarified derived bindings (for PIDE reports);
2016-06-21, by wenzelm
clarified rendering (amending ae9330fdbc16);
2016-06-21, by wenzelm
tuned whitespace;
2016-06-21, by wenzelm
merged
2016-06-21, by wenzelm
position information for literal facts;
2016-06-21, by wenzelm
tuned;
2016-06-21, by wenzelm
tuned;
2016-06-21, by wenzelm
Multivariate_Analysis: add continuous_on_vec_lambda
2016-06-21, by hoelzl
Probability: show that measures form a complete lattice
2016-06-16, by hoelzl
move open_Collect_eq/less to HOL
2016-06-15, by hoelzl
move Conditional_Complete_Lattices to Main
2016-06-17, by hoelzl
Probability: introduce Hahn decomposition; use it to clean up Radon_Nikodym
2016-06-15, by hoelzl
Probability: tuned headers; cleanup Radon_Nikodym
2016-06-14, by hoelzl
read Java system properties from ISABELLE_CI_PROPERTIES
2016-06-21, by Lars Hupel
merged
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
prefer HOL definitions;
2016-06-20, by wenzelm
tuned proof;
2016-06-20, by wenzelm
misc tuning and modernization;
2016-06-20, by wenzelm
Merged
2016-06-20, by eberlm
Merged
2016-06-17, by eberlm
fps_from_poly → fps_of_poly
2016-06-17, by eberlm
Merged
2016-06-17, by eberlm
Various additions to polynomials, FPSs, Gamma function
2016-06-16, by eberlm
misc tuning and modernization;
2016-06-19, by wenzelm
benchmark build profile
2016-06-19, by Lars Hupel
killed dead code
2016-06-17, by blanchet
avoid runtime warning with discriminators due to 'Code.del_eqn'
2016-06-17, by blanchet
killed deadcode
2016-06-17, by blanchet
be more careful before filtering out chained facts in Sledgehammer
2016-06-17, by blanchet
normalising multiset theorem names
2016-06-17, by fleury
tuned;
2016-06-16, by wenzelm
isabelle update_cartouches -c -t;
2016-06-16, by wenzelm
tuned;
2016-06-16, by wenzelm
Removed instances of ^ from theory markup
2016-06-16, by paulson
Urysohn's lemma, Dugundji extension theorem and many other proofs
2016-06-15, by paulson
non-deprecated char literals for Scala
2016-06-14, by haftmann
explicit resolution of ambiguous dictionaries
2016-06-14, by haftmann
Merge
2016-06-14, by paulson
new results about topology
2016-06-14, by paulson
Merged
2016-06-14, by eberlm
Integration by substitution
2016-06-14, by eberlm
tuned;
2016-06-14, by wenzelm
tuned;
2016-06-13, by wenzelm
Integral form of Gamma function
2016-06-13, by eberlm
Facts about HK integration, complex powers, Gamma function
2016-06-13, by eberlm
tuned
2016-06-13, by Lars Hupel
tuned;
2016-06-13, by wenzelm
tuned;
2016-06-12, by wenzelm
tuned;
2016-06-11, by wenzelm
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
2016-06-11, by haftmann
merged
2016-06-11, by Lars Hupel
start moving actual Jenkins build scripts into the repository
2016-06-11, by Lars Hupel
tuned order for isar-ref;
2016-06-11, by wenzelm
clarified;
2016-06-11, by wenzelm
clarified syntax;
2016-06-11, by wenzelm
spelling;
2016-06-11, by wenzelm
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
2016-06-10, by wenzelm
added command 'unbundle';
2016-06-10, by wenzelm
Merge
2016-06-10, by paulson
code to catch exception TERM in blast
2016-06-10, by paulson
merged
2016-06-10, by wenzelm
avoid duplicate Attrib.local_notes in aux. context;
2016-06-10, by wenzelm
proper restore;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
tuned;
2016-06-10, by wenzelm
prefer hybrid 'bundle' command;
2016-06-10, by wenzelm
documentation;
2016-06-09, by wenzelm
clarified;
2016-06-09, by wenzelm
support for bundle definition via target;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
tuned signature;
2016-06-09, by wenzelm
tuned;
2016-06-09, by wenzelm
Better treatment of assumptions/goals that are simply Boolean variables. Also cosmetic changes.
2016-06-10, by paulson
merged
2016-06-09, by immler
approximation, derivative, and continuity of floor and ceiling
2016-06-09, by immler
remove smt call in Lebesge_Measure
2016-06-09, by hoelzl
proper noWordSep as in "isabelle" mode (cf. 5024d0c48e02);
2016-06-08, by wenzelm
merged
2016-06-08, by wenzelm
NEWS;
2016-06-08, by wenzelm
tuned proofs;
2016-06-08, by wenzelm
provide dynamic facts in static context, to allow use of method_facts during static closure;
2016-06-08, by wenzelm
tuned;
2016-06-08, by wenzelm
clarified signature;
2016-06-07, by wenzelm
less ambitious arguments: thms only, no context declaration;
2016-06-07, by wenzelm
added method operator "use";
2016-06-07, by wenzelm
clarified signature;
2016-06-07, by wenzelm
clean facts more uniformly;
2016-06-07, by wenzelm
expode method_facts via dynamic method context;
2016-06-07, by wenzelm
tuned;
2016-06-07, by wenzelm
generalized bitlen to floor of log
2016-06-08, by immler
repair Unicode mess-up in c493859d4267
2016-06-08, by Andreas Lochbihler
NEWS and CONTRIBUTORS for SPMF
2016-06-08, by Andreas Lochbihler
merged
2016-06-08, by Andreas Lochbihler
import wasysym needed by Rewrite.thy
2016-06-07, by Andreas Lochbihler
add theory of discrete subprobability distributions
2016-06-07, by Andreas Lochbihler
clear distinction between different situations concerning strictness of code equations
2016-06-06, by haftmann
tuned signature
2016-06-06, by haftmann
more correct exception handling
2016-06-06, by haftmann
explicit tagging of code equations de-baroquifies interface
2016-06-06, by haftmann
dropped unused code
2016-06-06, by haftmann
conventional syntax for unit abstractions
2016-06-06, by haftmann
added action "isabelle.select-entity";
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
clarified focus_defs vs. focus_refs, e.g. relevant for @{here} where this overlaps;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
less redundant exploration of full name space;
2016-06-06, by wenzelm
tuned;
2016-06-06, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-480
+480
+1000
+3000
+10000
tip