isabelle: Graph

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
avoid multiple reports on shared type;
2016-06-06, by wenzelm
updated to recent changes of Poly/ML directory layout;
2016-06-04, by wenzelm
tuned;
2016-06-04, by wenzelm
Integer.lcm normalizes the sign as in HOL/GCD.thy;
2016-06-04, by wenzelm
support for .scala tools;
2016-06-03, by wenzelm
move ennreal and ereal theorems from MFMC_Countable
2016-06-02, by hoelzl
more flexible build_selection;
2016-06-03, by wenzelm
clarified aliases (no warning for duplicates);
2016-06-02, by wenzelm
eliminated pointless alias (no warning for duplicates);
2016-06-02, by wenzelm
avoid warnings on duplicate rules in the given list;
2016-06-02, by wenzelm
avoid stateful operations in virtual bootstrap, which presumably causes occasional crash of drule.ML due to inner syntax pp;
2016-06-02, by wenzelm
Hid RBT.filter
2016-06-02, by Manuel Eberl
proper ceil operation;
2016-06-01, by wenzelm
tuned;
2016-06-01, by wenzelm
isabelle components_checksum -u;
2016-06-01, by wenzelm
more documentation;
2016-06-01, by wenzelm
updated to jdk-8u92;
2016-06-01, by wenzelm
merged
2016-06-01, by wenzelm
NEWS;
2016-06-01, by wenzelm
more adhoc overloading;
2016-06-01, by wenzelm
clarified exception -- actually reject denominator = 0;
2016-06-01, by wenzelm
ML pp for Rat.rat;
2016-06-01, by wenzelm
clarified string_of_rat operations;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
clarified signature;
2016-06-01, by wenzelm
prefer rat numberals;
2016-06-01, by wenzelm
support rat numerals via special antiquotation syntax;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
tuned;
2016-06-01, by wenzelm
tuned signature;
2016-06-01, by wenzelm
maintain invariant for exported operation;
2016-05-31, by wenzelm
prefer more efficient Poly/ML operations, taking care of sign;
2016-05-31, by wenzelm
ad-hoc overloading for standard operations on type Rat.rat;
2016-05-31, by wenzelm
rat.ML is now part of Pure to allow tigther integration with Isabelle/ML;
2016-05-31, by wenzelm
Merged
2016-06-01, by eberlm
Tuned code equations for mappings and PMFs
2016-06-01, by eberlm
Added code generation for PMFs
2016-05-31, by eberlm
merged
2016-05-31, by traytel
moved lemma from afp
2016-05-31, by traytel
ignore Maven build products
2016-05-31, by Lars Hupel
added test
2016-05-31, by blanchet
made parsing of monomorphic/polymorphic constants more robust
2016-05-31, by blanchet
more flexible parsing (towards type class support)
2016-05-31, by blanchet
error message
2016-05-31, by blanchet
allow multiple recursive methods to co-exist in order to support mutual recursion;
2016-05-31, by matichuk
apply current morphism to method text before evaluating;
2016-05-30, by matichuk
merged
2016-05-30, by wenzelm
tuned;
2016-05-30, by wenzelm
allow 'for' fixes for multi_specs;
2016-05-30, by wenzelm
unused;
2016-05-30, by wenzelm
clarified check_open_spec / read_open_spec;
2016-05-29, by wenzelm
tuned;
2016-05-28, by wenzelm
clarified 'axiomatization';
2016-05-28, by wenzelm
clarified axiomatization;
2016-05-28, by wenzelm
clarified axiomatization: proper variables (!);
2016-05-28, by wenzelm
explicit check that abstract constructors cannot be part of official interface
2016-05-29, by haftmann
do not export abstract constructors in code_reflect
2016-05-29, by haftmann
added subtheory of longest common prefix
2016-05-29, by nipkow
tuned proofs;
2016-05-27, by wenzelm
tuned proofs;
2016-05-27, by wenzelm
tuned proofs, to allow unfold_abs_def;
2016-05-27, by wenzelm
clarified "unfold" operations;
2016-05-27, by wenzelm
tuned proof;
2016-05-27, by wenzelm
isabelle update_cartouches -c -t;
2016-05-26, by wenzelm
tuned spelling;
2016-05-26, by wenzelm
examples and documentation for code generator time measurements
2016-05-26, by haftmann
optional timing for code generator conversions
2016-05-26, by haftmann
clarified internal interfaces
2016-05-26, by haftmann
tuned
2016-05-26, by haftmann
delegate inclusion of required dictionaries to user-space instead of half-working magic
2016-05-26, by haftmann
corrected closure scope of static_conv_thingol;
2016-05-26, by haftmann
clarified proof context vs. background theory
2016-05-26, by haftmann
explicit quasi-global context for nbe conversions -- works around quasi-global type variable handling in lift_triv_classes_conv
2016-05-26, by haftmann
clarified naming conventions and code for code evaluation sandwiches
2016-05-26, by haftmann
clarified names of variants
2016-05-26, by haftmann
added function "prefixes" and some lemmas
2016-05-26, by nipkow
Merge
2016-05-25, by paulson
Merge
2016-05-25, by paulson
moved two theorems
2016-05-25, by paulson
updated proof of Residue Theorem (form Wenda Li)
2016-05-25, by paulson
merged
2016-05-25, by nipkow
renamed suffix(eq)
2016-05-25, by nipkow
updated 'define';
2016-05-25, by wenzelm
merged
2016-05-25, by wenzelm
isabelle update_cartouches -c -t;
2016-05-25, by wenzelm
isabelle update_cartouches -c -t;
2016-05-25, by wenzelm
NEWS: Permutations of a set and randomised folds
2016-05-25, by eberlm
new Isabelle component for CI infastructure
2016-05-24, by Lars Hupel
merged
2016-05-24, by wenzelm
recovered printing of DIM('a) (cf. 899c9c4e4a4c);
2016-05-24, by wenzelm
updated;
2016-05-24, by wenzelm
simplified syntax;
2016-05-24, by wenzelm
clarified syntax category names according to Isabelle/ML/Scala;
2016-05-24, by wenzelm
simplified syntax: Parse.term corresponds to Args.term etc.;
2016-05-24, by wenzelm
clarified syntax categories;
2016-05-24, by wenzelm
cartouche abbreviations work both for " as well;
2016-05-24, by wenzelm
Removed problematic code equation for set_permutations
2016-05-24, by eberlm
Backed out changeset 8230358fab88
2016-05-24, by eberlm
Deleted problematic code equation in Codegenerator_Test
2016-05-24, by eberlm
Merge
2016-05-24, by paulson
New theory for Homeomorphisms
2016-05-24, by paulson
Merge
2016-05-24, by paulson
renamings and new material
2016-05-24, by paulson
new theorem
2016-05-24, by paulson
deleted stray thm command
2016-05-23, by paulson
deleted needless comment
2016-05-23, by paulson
Resolved cyclic dependency of theories
2016-05-24, by eberlm
Merged
2016-05-24, by eberlm
Added set permutations/random permutations
2016-05-24, by eberlm
merged
2016-05-24, by wenzelm
embedded content may be delimited via cartouches;
2016-05-23, by wenzelm
tuned;
2016-05-23, by wenzelm
merged
2016-05-23, by nipkow
renamed prefix* in Library/Sublist
2016-05-23, by nipkow
generate Vampire 4.0 compatible output
2016-05-23, by blanchet
Merge
2016-05-23, by paulson
Lots of new material for multivariate analysis
2016-05-23, by paulson
removed odd cases rule (see also 8cb42cd97579);
2016-05-23, by wenzelm
tuned proofs;
2016-05-23, by wenzelm
tuned document;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
proper document source;
2016-05-23, by wenzelm
misc tuning and modernization;
2016-05-23, by wenzelm
merged
2016-05-21, by nipkow
added timing lemmas
2016-05-21, by nipkow
uniformly continuous function extended continuously on closure
2016-05-20, by immler
reduce isUCont to uniformly_continuous_on
2016-05-20, by immler
removed smt proof
2016-05-20, by immler
better handling of veriT's 'unknown' status
2016-05-20, by fleury
Resolved name clash
2016-05-18, by Manuel Eberl
Merged
2016-05-17, by eberlm
Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-17, by eberlm
Library: add partition_on
2016-05-17, by hoelzl
proper consideration of chained facts in 'try0' minimization
2016-05-17, by blanchet
re-enable fact index for 'obtains' assumption (amending 5c8e6a751adc);
2016-05-14, by wenzelm
tuned;
2016-05-14, by wenzelm
toplevel theorem statements support 'if'/'for' eigen-context;
2016-05-14, by wenzelm
reverted accidental commit;
2016-05-14, by wenzelm
eliminated use of empty "assms";
2016-05-13, by wenzelm
more complete theories;
2016-05-13, by wenzelm
common entity definitions within a global or local theory context;
2016-05-12, by wenzelm
clarified heading
2016-05-12, by haftmann
a quasi-recursive characterization of the multiset order (by Christian Sternagel)
2016-05-12, by haftmann
merged
2016-05-12, by wenzelm
avoid spurious fact index, notably in "context begin" (via Bundle.context);
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
tuned;
2016-05-12, by wenzelm
expose Sessions.Info in Build.Results
2016-05-12, by Lars Hupel
introduced class topological_group between topological_monoid and real_normed_vector
2016-05-11, by immler
find dynamic facts as well, but static ones are preferred;
2016-05-10, by wenzelm
some slight generalizations
2016-05-10, by immler
Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman
2016-05-10, by paulson
two new lemmas about segments
2016-05-10, by paulson
Merge
2016-05-09, by paulson
lemmas about dimension, hyperplanes, span, etc.
2016-05-09, by paulson
merged
2016-05-09, by wenzelm
clarified context, notably for internal use of Simplifier;
2016-05-09, by wenzelm
renamings and refinements
2016-05-09, by paulson
move Stirling numbers from AFP/Discrete_Summation
2016-05-04, by hoelzl
the standard While-rule
2016-05-01, by nipkow
re-tuned c9605a284fba, which impacts performance significantly (for unclear reasons) -- make AFP/Collections build again;
2016-04-29, by wenzelm
unfold is subject to unfold_abs_def (still inactive);
2016-04-28, by wenzelm
tuned;
2016-04-28, by wenzelm
NEWS;
2016-04-28, by wenzelm
clarified order: params/prems/concl interchangeable with !!/==> proposition;
2016-04-28, by wenzelm
support 'assumes' in specifications, e.g. 'definition', 'inductive';
2016-04-28, by wenzelm
tuned;
2016-04-27, by wenzelm
merged
2016-04-26, by wenzelm
updated subtle side-conditions;
2016-04-26, by wenzelm
some uses of 'obtain' with structure statement;
2016-04-26, by wenzelm
'obtain' supports structured statements (similar to 'define');
2016-04-26, by wenzelm
more portable: GNU find no longer supports "-perm +mode";
2016-04-26, by wenzelm
more uniform operations for structured statements;
2016-04-26, by wenzelm
defs are closed, which leads to proper auto_bind_facts;
2016-04-26, by wenzelm
tuned notation;
2016-04-26, by wenzelm
misc tuning and modernization;
2016-04-26, by wenzelm
Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
2016-04-22, by hoelzl
Linear_Algebra: alternative representation of linear combination
2016-04-22, by hoelzl
Linear_Algebra: move abstract concepts to front
2016-04-22, by hoelzl
merge
2016-04-25, by blanchet
avoid duplicate mixfix messages in '(co)datatype' type name
2016-04-25, by blanchet
generalize code to avoid making assumptions about type variable names
2016-04-25, by blanchet
intermediate definitions and caching in n2m to keep terms small
2016-04-15, by traytel
n2m operates on (un)folds
2016-04-14, by traytel
clarified rendering;
2016-04-25, by wenzelm
old 'def' is legacy;
2016-04-25, by wenzelm
more rigid check of lhs;
2016-04-25, by wenzelm