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.
make mangling sound w.r.t. type arguments
20110907, by blanchet
make "filter_type_args" more robust if the actual arity is higher than the declared one
20110907, by blanchet
updated Sledgehammer documentation
20110907, by blanchet
rationalize uniform encodings
20110907, by blanchet
merged
20110906, by huffman
avoid using legacy theorem names
20110906, by huffman
merged
20110906, by huffman
remove redundant lemmas i_mult_eq and i_mult_eq2 in favor of i_squared
20110906, by huffman
HOL/Import: Update HOL4 generated files to current Isabelle.
20110907, by Cezary Kaliszyk
tuned proofs;
20110907, by wenzelm
remove some unnecessary simp rules from simpset
20110906, by huffman
some Isabelle/jEdit NEWS;
20110906, by wenzelm
more README;
20110906, by wenzelm
merged
20110906, by wenzelm
merged
20110906, by huffman
simplify proof of tan_half, removing unused assumptions
20110906, by huffman
convert some proofs to Isarstyle
20110906, by huffman
added dummy polymorphic THF system
20110906, by blanchet
added some examples for pattern and weight annotations
20110906, by boehmes
merged
20110906, by bulwahn
avoid "Code" as structure name (cf. 3bc39cfe27fe)
20110906, by bulwahn
remove duplicate copy of lemma sqrt_add_le_add_sqrt
20110906, by huffman
remove redundant lemma real_sum_squared_expand in favor of power2_sum
20110906, by huffman
remove redundant lemma LIMSEQ_Complex in favor of tendsto_Complex
20110906, by huffman
merged
20110906, by huffman
add lemmas about arctan;
20110905, by huffman
convert lemma cos_total to Isarstyle proof
20110905, by huffman
added new lemmas
20110906, by nipkow
updated Sledgehammer's docs
20110906, by blanchet
cleanup "simple" type encodings
20110906, by blanchet
merge
20110906, by Cezary Kaliszyk
HOL/Import: Make HOL4 Import work with current Isabelle. Updated constant maps, added bool type map, and tuned compat theorem.
20110906, by Cezary Kaliszyk
tuning
20110906, by blanchet
drop more type arguments soundly, when they can be deduced from the arg types
20110906, by blanchet
bulk reports for improved message throughput;
20110906, by wenzelm
bulk reports for improved message throughput;
20110906, by wenzelm
tuned signature;
20110906, by wenzelm
more specific message channels to avoid potential bottleneck of raw_messages;
20110906, by wenzelm
buffer prover messages to prevent overloading of session_actor input channel  which is critical due to synchronous messages wrt. GUI thread;
20110906, by wenzelm
more abstract receiver interface;
20110906, by wenzelm
flush after Output.raw_message (and init message) for reduced latency of important protocol events;
20110906, by wenzelm
convert lemma cos_is_zero to Isarstyle
20110905, by huffman
merged
20110905, by huffman
convert lemma sin_gt_zero to Isar style;
20110905, by huffman
modify lemma sums_group, and shorten proofs that use it
20110905, by huffman
generalize some lemmas
20110905, by huffman
add lemmas cos_arctan and sin_arctan
20110905, by huffman
tuned indentation
20110905, by huffman
more visible outdated_color;
20110905, by wenzelm
commands_change_delay within main actor  prevents overloading of commands_change_buffer input channel;
20110905, by wenzelm
tuned imports;
20110905, by wenzelm
fixed handling of "sledgehammer_params", so that "sledgehammer_params [e]" is really the same as "sledgehammer_params [provers = e]"
20110905, by blanchet
tuned
20110905, by boehmes
tuned
20110905, by boehmes
filter out all schematic theorems if the problem contains no ground constants
20110905, by boehmes
merged
20110904, by huffman
tuned comments
20110904, by huffman
simplify proof of Bseq_mono_convergent
20110904, by huffman
merged
20110904, by wenzelm
replace lemma expi_imaginary with reoriented lemma cis_conv_exp
20110904, by huffman
less
more

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