Mercurial
Mercurial
>
repos
>
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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
adding type inference for disambiguation annotations in code equation
20110907, by bulwahn
adding the body type as well to the code generation for constants as it is required for type annotations of constants
20110907, by bulwahn
changing const type to pass along if typing annotations are necessary for disambigous terms
20110907, by bulwahn
fixed THF type constructor syntax
20110907, by blanchet
tweaking polymorphic TFF and THF output
20110907, by blanchet
parse new experimental '@' encodings
20110907, by blanchet
tuning
20110907, by blanchet
tuning
20110907, by blanchet
tuning
20110907, by blanchet
clarified import;
20110907, by wenzelm
tuned/simplified proofs;
20110907, by wenzelm
tuned proofs;
20110907, by wenzelm
deactivate unfinished charset provider for now, to avoid user confusion;
20110907, by wenzelm
more NEWS;
20110907, by wenzelm
added "check" button: adhoc change to full buffer perspective;
20110907, by wenzelm
added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
20110907, by wenzelm
separate mangling, which can (and should) be done before the formulas are firstorderized, and type arg filtering, which must be done after once the min arities have been computed
20110907, by blanchet
perform mangling before computing symbol arity, to avoid needless "hAPP"s and "hBOOL"s
20110907, by blanchet
tuning
20110907, by blanchet
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
remove redundant lemmas expi_add and expi_zero
20110904, by huffman
remove redundant lemmas about LIMSEQ
20110904, by huffman
introduce abbreviation 'int' earlier in Int.thy
20110904, by huffman
remove unused assumptions from natceiling lemmas
20110904, by huffman
move lemmas nat_le_iff and nat_mono into Int.thy
20110904, by huffman
eliminated markup for plain identifiers (frequent but insignificant);
20110904, by wenzelm
simplified signatures;
20110904, by wenzelm
synchronous XML.Cache without actor  potentially more efficient on machines with few cores;
20110904, by wenzelm
tuned document;
20110904, by wenzelm
improved handling of extended styles and hard tabs when prover is inactive;
20110904, by wenzelm
mark hard tabs as single chunks, as required by jEdit;
20110904, by wenzelm
updated READMEs;
20110904, by wenzelm
property "tooltipdismissdelay" is edited in ms, not seconds;
20110904, by wenzelm
moved XML/YXML to src/Pure/PIDE;
20110904, by wenzelm
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
20110904, by wenzelm
pseudodefinition for perms on sets; tuned
20110904, by haftmann
remove duplicate lemma nat_zero in favor of nat_0
20110903, by huffman
merged
20110903, by huffman
merged
20110903, by huffman
modify nominal packages to better respect set/pred distinction
20110903, by huffman
merged
20110903, by huffman
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
less
more

(0)
30000
10000
3000
1000
120
+120
+1000
+3000
+10000
tip