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.
more precise treatment of nodes that are fully required for partially visible ones;
20110827, by wenzelm
deassigned commands also count as changed;
20110827, by wenzelm
beef up sledgehammer_tac in Mirabelle some more
20110827, by blanchet
merged
20110827, by blanchet
change default for generation of tag idempotence and tag argument equations
20110826, by blanchet
merged
20110826, by huffman
NEWS entry for setsum_norm ~> norm_setsum
20110826, by huffman
make HOLProbability respect set/pred distinction
20110826, by huffman
merged
20110826, by wenzelm
use rename_tac to make proof script more robust (with separate set type, 'clarify' yields different variable names)
20100908, by huffman
merged
20110826, by huffman
generalize and simplify proof of continuous_within_sequentially
20110826, by huffman
add lemma sequentially_imp_eventually_within;
20110826, by huffman
replace some continuous_on lemmas with more general versions
20110825, by huffman
remove legacy theorem Lim_inner
20110825, by huffman
arrange everything related to ordered_euclidean_space class together
20110825, by huffman
generalize and shorten proof of basis_orthogonal
20110825, by huffman
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
20110825, by huffman
merged
20110825, by huffman
generalize lemma finite_imp_compact_convex_hull and related lemmas
20110825, by huffman
generalize some lemmas
20110825, by huffman
generalize lemma convex_cone_hull
20110825, by huffman
rename subset_{interior,closure} to {interior,closure}_mono;
20110825, by huffman
simplify many proofs about subspace and span;
20110825, by huffman
remove duplicate simp declaration
20110825, by huffman
simplify definition of 'interior';
20110825, by huffman
add lemma closure_union;
20110824, by huffman
minimize imports
20110824, by huffman
move everything related to 'norm' method into new theory file Norm_Arith.thy
20110824, by huffman
remove unused lemmas dimensionI, dimension_eq
20110824, by huffman
move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
20110824, by huffman
merge
20110826, by Cezary Kaliszyk
FSet: Explicit proof without mem_def
20110826, by Cezary Kaliszyk
merged
20110826, by nipkow
added lemma
20110826, by nipkow
added a component in generated file names reflecting whether the minimizer is used  needed for evaluation to keep these files separated from the main problem files
20110826, by blanchet
comment
20110826, by blanchet
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
20110826, by blanchet
improve completeness of polymorphic encodings
20110826, by blanchet
mangle tag bound declarations properly
20110826, by blanchet
fixed inverted logic and improve precision when handling monotonic types in polymorphic encodings
20110826, by blanchet
make sure that if slicing is disabled, a nonSOS slice is chosen
20110825, by blanchet
honor TFF Implicit
20110825, by blanchet
make polymorphic encodings more complete
20110825, by blanchet
make default unsound mode less unsound
20110825, by blanchet
make TFF output less explicit where possible
20110825, by blanchet
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
20110825, by blanchet
added one more known Z3 failure
20110825, by blanchet
added config options to control two aspects of the translation, for evaluation purposes
20110825, by blanchet
added choice operator output for
20110825, by nik
rationalized option names  mono becomes raw_mono and mangled becomes mono
20110825, by blanchet
handle nonmangled monomorphich the same way as mangled monomorphic when it comes to helper  otherwise we can end up generating too tight type guards
20110825, by blanchet
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
20110825, by blanchet
fixed bang encoding detection of which types to encode
20110825, by blanchet
lemma Compl_insert: " insert x A = (A)  {x}"
20110825, by krauss
avoid variable clashes by properly incrementing indices
20110825, by boehmes
improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
20110825, by boehmes
include chained facts for minimizer, otherwise it won't work
20110825, by blanchet
remove Vampire imconplete proof detection  the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
20110824, by blanchet
back to tradition Scratch.thy default  execution wrt. perspective overcomes the main problems of 226563829580;
20110826, by wenzelm
less
more

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