Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
20180301, by wenzelm
merged
20180228, by immler
generalized lemmas about orthogonal transformation
20180228, by immler
more explicit infixl (see initial 1edf0f223c6e);
20180228, by wenzelm
clarified use of vec type syntax;
20180228, by wenzelm
new lemma
20180226, by haftmann
dedicated append function for string literals
20180226, by haftmann
generalized
20180226, by immler
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
20180226, by immler
merged
20180225, by wenzelm
prefer symbols;
20180225, by wenzelm
tuned;
20180225, by wenzelm
more abbrevs;
20180225, by wenzelm
allow multiple entries of and_list (on both sides);
20180225, by wenzelm
eliminated ASCII syntax from Pure bootstrap;
20180225, by wenzelm
merged
20180225, by paulson
new material on matrices, etc., and consolidating duplicate results about of_nat
20180225, by paulson
notation for dummy sort;
20180225, by wenzelm
more symbols;
20180224, by wenzelm
merged
20180223, by wenzelm
tuned signature;
20180223, by wenzelm
tuned signature;
20180223, by wenzelm
tuned signature;
20180223, by wenzelm
removed unused clone of (map o apsnd);
20180223, by wenzelm
prefer existing HOLogic.mk_obj_eq, despite subtle semantic differences of COMP vs. RS;
20180223, by wenzelm
added HOLogic.mk_obj_eq convenience and eliminated some clones;
20180223, by wenzelm
tuned  use existing Morphism.instantiate_morphism;
20180223, by wenzelm
Merged;
20180223, by Wenda Li
merged
20180223, by Wenda Li
Unified the order of zeros and poles; improved reasoning around nonessential singularites
20180223, by Wenda Li
merged
20180223, by wenzelm
tuned;
20180223, by wenzelm
tuned signature  eliminated clones;
20180223, by wenzelm
command 'interpret' no longer exposes resulting theorems as literal facts;
20180223, by wenzelm
more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy;
20180223, by wenzelm
tuned;
20180222, by wenzelm
more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
20180221, by wenzelm
explicit operations to instantiate frees: typ, term, thm, morphism;
20180221, by wenzelm
more operations for ctyp, cterm;
20180221, by wenzelm
minor tuning and clarification;
20180221, by wenzelm
minor tuning and clarification;
20180220, by wenzelm
tuned signature;
20180220, by wenzelm
fixed the proof of pair_measure_count_space
20180223, by paulson
merged
20180223, by paulson
fixing ennreal using add_mono1; shifting results from linordered_semidom to linordered_nonzero_semiring
20180223, by paulson
merged
20180222, by paulson
type class linordered_nonzero_semiring has new axiom to guarantee characteristic 0
20180222, by paulson
simplified Radix_Sort
20180223, by nipkow
merged
20180222, by immler
merged
20180222, by immler
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
20180222, by immler
simplified def of stable
20180222, by nipkow
Lots of new material about matrices, etc.
20180221, by paulson
tuned proofs  prefer explicit names for facts from 'interpret';
20180220, by wenzelm
merged
20180220, by wenzelm
eliminated questionable Par_List.map  locale interpretation is mostly lazy (see also b81f1de9f57e);
20180220, by wenzelm
tuned signature;
20180220, by wenzelm
tuned;
20180220, by wenzelm
use lazy notes for locale context init and later additions of facts;
20180220, by wenzelm
avoid premature Lazy.force due to strict "?" operator;
20180220, by wenzelm
less
more

(0)
30000
10000
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
tip