isabelle: Graph

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
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
2016-04-25, by wenzelm
eliminated old 'def';
2016-04-25, by wenzelm
added Isar command 'define';
2016-04-24, by wenzelm
within a proof body context, undeclared frees are like global constants;
2016-04-24, by wenzelm
clarified modules;
2016-04-24, by wenzelm
added "balanced" predicate
2016-04-22, by nipkow
fixed code equation for pdivmod, added improved code equation for pseudo_mod
2016-04-20, by Rene Thiemann
proper latex;
2016-04-20, by wenzelm
merged
2016-04-20, by wenzelm
reactivated other_id reports (see also db929027e701, 8eda56033203);
2016-04-20, by wenzelm
invisible context similar to interpretation;
2016-04-20, by wenzelm
avoid massive multiplication of reports due to interpretation;
2016-04-20, by wenzelm
tuned comments;
2016-04-19, by wenzelm
more thorough update;
2016-04-19, by wenzelm
several updates on polynomial long division and pseudo division
2016-04-15, by Rene Thiemann
fragment of a HOL type class primer
2016-04-18, by haftmann
capitalized GCD and LCM syntax
2016-04-18, by haftmann
environment variable check has become pointless after 771b8ad5c7fc
2016-04-18, by haftmann
unfold internal definitions before emitting a proof obligation
2016-04-19, by traytel
more IDE support for Isabelle/Pure bootstrap;
2016-04-19, by wenzelm
merged
2016-04-18, by wenzelm
tuned signature;
2016-04-18, by wenzelm
prefer internal attribute source;
2016-04-18, by wenzelm
tidying some proofs; getting rid of "nonempty_witness"
2016-04-18, by paulson
Merge
2016-04-18, by paulson
numerous theorems about affine hulls, hyperplanes, etc.
2016-04-18, by paulson
merged
2016-04-18, by wenzelm
proper LaTeX;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
clarified bindings;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
tuned;
2016-04-18, by wenzelm
avoid clash with function called "x";
2016-04-18, by wenzelm
new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-18, by paulson
clarified bindings;
2016-04-17, by wenzelm
clarified bindings;
2016-04-17, by wenzelm