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
+30000
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.
slightly more standard induct_simp_add/del attributes;
20100430, by wenzelm
map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
20100430, by wenzelm
export Simplifier.with_context;
20100430, by wenzelm
removed some old comments;
20100430, by wenzelm
merged
20100430, by huffman
merged
20100430, by huffman
generalize lemma adjoint_unique; simplify some proofs
20100429, by huffman
fix latex url
20100429, by huffman
merged
20100429, by huffman
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
20100429, by huffman
remove unused function vector_power, unused lemma one_plus_of_nat_neq_0
20100429, by huffman
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
20100429, by huffman
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
20100429, by huffman
generalize LIMSEQ_vector to tendsto_vector
20100428, by huffman
generalize orthogonal_clauses
20100428, by huffman
remove redundant lemma vector_dist_norm
20100428, by huffman
remove redundant lemma norm_0
20100428, by huffman
generalize some euclidean space lemmas
20100428, by huffman
prove lemma openin_subopen without using choice
20100428, by huffman
move pathrelated stuff into new theory file
20100428, by huffman
add new Multivariate_Analysis files to IsaMakefile
20100428, by huffman
move operator norm stuff to new theory file
20100428, by huffman
eliminated spurious sledgehammer invocation;
20100430, by wenzelm
merged
20100430, by wenzelm
merged
20100430, by haftmann
merged
20100430, by haftmann
enclose case expression in brackets
20100430, by haftmann
catch the right exception
20100430, by blanchet
eliminate trivial case splits from Isar proofs
20100430, by blanchet
remove debugging code
20100430, by blanchet
merged
20100430, by blanchet
minor improvements
20100430, by blanchet
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
20100430, by blanchet
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
20100430, by blanchet
in "overlord" mode: ignore problem prefix specified in the .thy file
20100429, by blanchet
uncomment code
20100429, by blanchet
redid some Sledgehammer/Metis proofs
20100429, by blanchet
fix more "undeclared symbol" errors related to SPASS's DFG format
20100429, by blanchet
be more discriminate: some oneline Isar proofs are silly
20100429, by blanchet
onestep Isar proofs are not always pointless
20100429, by blanchet
the SPASS output syntax is more general than I thought  such a pity that there's no documentation
20100429, by blanchet
redo more Metis/Sledgehammer example
20100429, by blanchet
fixed definition of "bad frees" so that it actually works
20100429, by blanchet
don't remove last line of proof
20100429, by blanchet
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
20100429, by blanchet
make SML/NJ happy, take 2
20100429, by blanchet
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
20100429, by blanchet
expand combinators in Isar proofs constructed by Sledgehammer;
20100429, by blanchet
more neg_clausify proofs that get replaced by direct proofs
20100429, by blanchet
redo some of the metis proofs
20100428, by blanchet
back to Vampire 9  Vampire 11 sometimes outputs really weird proofs
20100428, by blanchet
improve unskolemization
20100428, by blanchet
make sure short theorem names are preferred to composite ones in Sledgehammer;
20100428, by blanchet
properly extract SPASS proof
20100428, by blanchet
try out Vampire 11 and parse its output correctly;
20100428, by blanchet
return updated info record after termination proof
20100430, by krauss
proper context for rule_by_tactic;
20100430, by wenzelm
conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
20100430, by wenzelm
hgweb style: show author in filelog; full description in annotate hover
20100429, by krauss
proper context for mksimps etc.  via simpset of the running Simplifier;
20100429, by wenzelm
less
more

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