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.
added fun flip f x y = f y x
20070511, by krauss
generalize setsum lemmas from semiring_0_cancel to semiring_0
20070511, by huffman
tuned proofs;
20070511, by wenzelm
bang_facts: warning;
20070511, by wenzelm
tuned proofs;
20070511, by wenzelm
(class target)
20070510, by haftmann
cleaned up
20070510, by haftmann
beta/eta conversion after preprocessor
20070510, by haftmann
fixed typo
20070510, by haftmann
more conversions;
20070510, by wenzelm
Moved extraction_expand declaration of listall_def outside of definition.
20070510, by berghofe
Adapted to new naming scheme for definitions.
20070510, by berghofe
Changed name of raw definition.
20070510, by berghofe
Name of ML function "not" is now qualified in order to avoid
20070510, by berghofe
consts in consts_code Isar commands are now referred to by usual term syntax
20070510, by haftmann
size [nat] is identity
20070510, by haftmann
explicit import of Datatype.thy due to hook bootstrap problem
20070510, by haftmann
localized Sup/Inf
20070510, by haftmann
localized Min/Max
20070510, by haftmann
tuned
20070510, by haftmann
fix proofs
20070510, by huffman
remove redundant lemmas
20070510, by huffman
lemmas iszero_(h)complex_number_of are no longer needed
20070510, by huffman
instance real_algebra_1 < ring_char_0
20070510, by huffman
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
20070510, by huffman
moved conversions to structure Conv;
20070510, by wenzelm
added dest_fun/fun2/arg1;
20070510, by wenzelm
tuned argument_type_of;
20070510, by wenzelm
added destructors from drule.ML;
20070510, by wenzelm
moved some operations to more_thm.ML and conv.ML;
20070510, by wenzelm
Conversions: primitive equality reasoning (from drule.ML);
20070510, by wenzelm
added conv.ML;
20070510, by wenzelm
Thm.match;
20070510, by wenzelm
moved some Drule operations to Thm (see more_thm.ML);
20070510, by wenzelm
Thm.first_order_match;
20070510, by wenzelm
moved conversions to structure Conv;
20070510, by wenzelm
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
20070509, by krauss
add lemma norm_diff_ineq; shorten other proofs
20070509, by huffman
removed Complex/ComplexBin.thy;
20070509, by wenzelm
tuned ML setup;
20070509, by wenzelm
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
less
more

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