Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
tuned syntax;
20070509, by wenzelm
eliminated unnamed infixes;
20070509, by wenzelm
removed unused mk_cond_defpair;
20070509, by wenzelm
simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multithreaded simplification);
20070509, by wenzelm
remove empty, unused theory
20070509, by huffman
remove redundant lemmas
20070509, by huffman
add lemma hnorm_hyperpow
20070509, by huffman
add lemma of_hypreal_hyperpow
20070509, by huffman
tuned
20070509, by haftmann
moved recfun_codegen.ML to Code_Generator.thy
20070509, by haftmann
continued
20070509, by haftmann
remove redundant lemmas
20070509, by huffman
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
20070509, by huffman
add lemma hnorm_divide
20070509, by huffman
add lemmas abs_hnorm_cancel, hnorm_of_hypreal
20070509, by huffman
add lemmas norm_add_less, norm_mult_less
20070509, by huffman
add lemma Standard_hyperpow
20070508, by huffman
tuned;
20070508, by wenzelm
add of_hypreal constant with lemmas
20070508, by huffman
add lemmas norm_number_of, norm_of_int, norm_of_nat
20070508, by huffman
quoted 'declaration';
20070508, by wenzelm
simplified pretty_thm(_legacy);
20070508, by wenzelm
is_sid: include '::';
20070508, by wenzelm
tuned ProofDisplay.pretty_full_theory;
20070508, by wenzelm
tuned;
20070508, by wenzelm
updated;
20070508, by wenzelm
simplified context data;
20070508, by wenzelm
tuned;
20070508, by wenzelm
legacy_intern_skolem: legacy_feature;
20070508, by wenzelm
tuned;
20070508, by wenzelm
renamed call_atp to sledgehammer;
20070508, by wenzelm
updated;
20070508, by wenzelm
tuned context data;
20070508, by wenzelm
ML adaptions
20070508, by haftmann
clean up complex norm proofs, remove redundant lemmas
20070508, by huffman
remove redundant lemmas
20070508, by huffman
fix proof of hypreal_sqrt_sum_squares_ge1
20070508, by huffman
add lemma real_sqrt_sum_squares_triangle_ineq
20070508, by huffman
add lemma abs_norm_cancel
20070508, by huffman
cleaned up
20070508, by huffman
polished some proofs
20070508, by urbanc
add lemmas power2_le_imp_le and power2_less_imp_less
20070508, by huffman
add lemma power_less_imp_less_base
20070508, by huffman
clean up RealVector classes
20070507, by huffman
Firstorder variant of the fullytyped translation
20070507, by paulson
added further equality example
20070507, by haftmann
changed 'code nofunc' to 'code func del'
20070507, by haftmann
* Context data interfaces;
20070507, by wenzelm
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
20070507, by wenzelm
simplified DataFun interfaces;
20070507, by wenzelm
changed code generator invocation syntax
20070506, by haftmann
PreList imports RecDef
20070506, by haftmann
dropped legacy ML binding
20070506, by haftmann
added auxiliary lemmas for proof tools
20070506, by haftmann
dropped preorders, unified syntax
20070506, by haftmann
minimal import
20070506, by haftmann
dropped HOL.ML
20070506, by haftmann
tuned
20070506, by haftmann
updated Alice version;
20070506, by wenzelm
IntInf.fromInt;
20070506, by wenzelm
less
more

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