Mercurial
Mercurial
>
repos
>
testboard
/ 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.
UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT  these rules appear to be applied to thms with fixed types only;
20100503, by wenzelm
replaced Thm.legacy_freezeT by Thm.unvarify_global  these facts stem from closed definitions, i.e. there are no term Vars;
20100503, by wenzelm
renamed Thm.freezeT to Thm.legacy_freezeT  it is based on Type.legacy_freeze;
20100503, by wenzelm
minor tuning of Thm.strip_shyps  no longer pervasive;
20100503, by wenzelm
simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
20100503, by wenzelm
old NEWS on global operations;
20100503, by wenzelm
ProofContext.init_global;
20100503, by wenzelm
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
20100503, by wenzelm
merged
20100503, by haftmann
do not generate code per default  touches file of parent session
20100430, by haftmann
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
20100501, by krauss
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
20100501, by krauss
now if this doesn't make SML/NJ happy, nothing will
20100501, by blanchet
more stats;
20100501, by wenzelm
renamed Variable.thm_context to Variable.global_thm_context to emphasize that this is not the real thing;
20100430, by wenzelm
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
less
more

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