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
+10000
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.
remove unused assumption from lemma posreal_complete
20110903, by huffman
tuned specifications
20110903, by haftmann
merged
20110903, by haftmann
tuned proof
20110903, by haftmann
merged
20110903, by haftmann
assert Pure equations for theorem references; avoid dynamic reference to fact
20110903, by haftmann
assert Pure equations for theorem references; tuned
20110903, by haftmann
tuned specifications and proofs
20110903, by haftmann
merged
20110903, by wenzelm
remove duplicate lemma finite_choice in favor of finite_set_choice
20110903, by huffman
simplify proof
20110903, by huffman
shorten some proofs
20110903, by huffman
remove redundant simp rules ceiling_floor and floor_ceiling
20110902, by huffman
misc tuning and simplification of proofs;
20110903, by wenzelm
Document.removed_versions on Scala side;
20110903, by wenzelm
discontinued predefined empty command (obsolete!?);
20110903, by wenzelm
discontinued global execs: store exec value directly within entries;
20110903, by wenzelm
Document.remove_versions on ML side;
20110903, by wenzelm
some support to prune_history;
20110903, by wenzelm
merged
20110902, by huffman
speed up extremely slow metis proof of Sup_real_iff
20110902, by huffman
remove redundant lemma reals_complete2 in favor of complete_real
20110902, by huffman
simplify proof of Rats_dense_in_real;
20110902, by huffman
remove unused, unnecessary lemmas
20110902, by huffman
remove more duplicate lemmas
20110902, by huffman
merged
20110902, by wenzelm
merged
20110902, by haftmann
avoid "Code" as structure name
20110902, by haftmann
more robust chunk painting wrt. hard tabs, when chunk.str == null;
20110902, by wenzelm
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
20110902, by wenzelm
less agressive parsing of commands (priority ~1);
20110902, by wenzelm
tuned;
20110902, by wenzelm
more direct Token.range_pos and Outer_Syntax.read_command, bypassing Thy_Syntax.span;
20110902, by wenzelm
merged
20110902, by nipkow
Added Abstract Interpretation theories
20110902, by nipkow
tuned proofs;
20110902, by wenzelm
proper config option linarith_trace;
20110902, by wenzelm
discontinued slightly odd "Defining record ..." message and corresponding quiet_mode;
20110902, by wenzelm
merged
20110902, by wenzelm
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
20110902, by blanchet
use new syntax for Pi binder in TFF1 output
20110902, by blanchet
fewer TPTP important messages
20110902, by blanchet
simplify some proofs about uniform continuity, and add some new ones;
20110901, by huffman
modernize lemmas about 'continuous' and 'continuous_on';
20110901, by huffman
add lemma tendsto_infnorm
20110901, by huffman
more precise iterate_entries_after if start refers to last entry;
20110902, by wenzelm
clarified define_command: store name as structural information;
20110902, by wenzelm
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
20110901, by wenzelm
more redable Document.Node.toString;
20110901, by wenzelm
sort wrt. theory name;
20110901, by wenzelm
modernized theory name;
20110901, by wenzelm
repaired benchmarks;
20110901, by wenzelm
merged
20110901, by wenzelm
tuning
20110901, by blanchet
always measure time for ATPs  auto minimization relies on it
20110901, by blanchet
added two lemmas about "distinct" to help Sledgehammer
20110901, by blanchet
make "sound" sound and "unsound" more sound, based on evaluation
20110901, by blanchet
HOL/Import: observe distinction between sets and predicates (where possible)
20110901, by Cezary Kaliszyk
simplify/generalize some proofs
20110831, by huffman
generalize lemma isCont_vec_nth
20110831, by huffman
less
more

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