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

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
prefer binding over base name;
2016-04-17, by wenzelm
clarified signature;
2016-04-17, by wenzelm
removed pointless check (see Type_Infer.object_logic);
2016-04-17, by wenzelm
prefer precise names for internal construction;
2016-04-17, by wenzelm
remove "slow" session tags
2016-04-17, by Lars Hupel
misc tuning and modernization;
2016-04-17, by wenzelm
clarified reported positions;
2016-04-17, by wenzelm
operate on proper binding;
2016-04-17, by wenzelm
tuned;
2016-04-17, by wenzelm
add "slow" group to descendants of HOL-Proofs
2016-04-15, by Lars Hupel
merged
2016-04-15, by wenzelm
support for Poly/ML entity ids;
2016-04-15, by wenzelm
clarified PIDE reports;
2016-04-15, by wenzelm
clarified rendering wrt. hyperlinks;
2016-04-15, by wenzelm
tuned -- no position;
2016-04-15, by wenzelm
clarified focus visibility;
2016-04-15, by wenzelm
tuned rendering;
2016-04-15, by wenzelm
highlighting of entity def/ref positions wrt. cursor;
2016-04-14, by wenzelm
background color for entity def/ref focus;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
more silence;
2016-04-14, by wenzelm
avoid misleading Simplifier trace in quickcheck, notably in auto quickcheck;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
clarified context;
2016-04-14, by wenzelm
misc tuning and standardization;
2016-04-14, by wenzelm
tuned headers;
2016-04-14, by wenzelm
fix HOL-Probability-ex
2016-04-15, by hoelzl
change is incompatible
2016-04-14, by hoelzl
Probability: move emeasure and nn_integral from ereal to ennreal
2016-04-14, by hoelzl
tuned;
2016-04-14, by wenzelm
clarified modules;
2016-04-14, by wenzelm
tuned;
2016-04-14, by wenzelm
back to exact copy of non-text file (amending dcc8e1d34b18);
2016-04-14, by wenzelm
merged
2016-04-13, by wenzelm
eliminated "xname" and variants;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
more completions, independently on accidental external form (e.g. "Map.empty" with its redundant prefix);
2016-04-13, by wenzelm
tuned;
2016-04-13, by wenzelm
clarified syntax;
2016-04-13, by wenzelm
avoid quotes for qualified names;
2016-04-13, by wenzelm
added rule
2016-04-13, by immler
tuned;
2016-04-12, by wenzelm
merged
2016-04-12, by wenzelm
simplified -- avoid odd mutable state, which potentially causes problems with module initialization;
2016-04-12, by wenzelm
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
2016-04-12, by wenzelm
Type_Infer.object_logic controls improvement of type inference result;
2016-04-12, by wenzelm
tuned;
2016-04-12, by wenzelm
simplified constraints;
2016-04-11, by wenzelm
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
2016-04-11, by wenzelm
tuned imports;
2016-04-11, by wenzelm
tuned message;
2016-04-11, by wenzelm
tuned;
2016-04-11, by wenzelm
added lemmas
2016-04-12, by immler
generalized
2016-04-12, by immler
added derivative of scaling in exponential function
2016-04-12, by immler
lots of new theorems for multivariate analysis
2016-04-11, by paulson
tuned;
2016-04-10, by wenzelm