isabelle: Graph

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

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