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.
tidying, removing obsolete lemmas about 0=...
20001220, by paulson
SML90: ord, chr, explode, implode;
20001220, by wenzelm
reorienting equations with #nnn on the lhs
20001219, by paulson
reorienting equations with 0, 1, 2 on the lhs
20001219, by paulson
new file extract_common_term.ML for the cancelfactor simprocs
20001219, by paulson
inserting the simproc nat_cancel_factor
20001219, by paulson
inserting the simproc int_cancel_factor
20001219, by paulson
new simprule zero_less_abs_iff
20001219, by paulson
coping with the reorientation of #nn=x
20001219, by paulson
cancelfactor simproc allows shorter proofs
20001219, by paulson
more tidying
20001219, by paulson
cancelfactor simproc allows a shorter proof
20001219, by paulson
improved errors;
20001219, by wenzelm
*** empty log message ***
20001218, by nipkow
*** empty log message ***
20001218, by nipkow
new simproc for cancelling common factors, etc.
20001218, by paulson
moved mk_bin from Numerals to HOLogic
20001218, by nipkow
added rational arithmetic
20001218, by nipkow
towards rtional arithmetic
20001218, by nipkow
tidying and adding new proofs
20001218, by paulson
loads the new simproc extract_common_term
20001218, by paulson
'def': \<equiv>;
20001216, by wenzelm
tuned HOL/Real/HahnBanach;
20001216, by wenzelm
'def': equiv;
20001216, by wenzelm
\isasymequiv;
20001216, by wenzelm
updated;
20001215, by wenzelm
corrected errors;
20001215, by bauerg
usedir m brackets;
20001215, by wenzelm
GPLed;
20001215, by wenzelm
tuned comment;
20001215, by wenzelm
restore \int (integral);
20001215, by wenzelm
tuned symbols;
20001215, by wenzelm
further round of tidying
20001215, by paulson
*** empty log message ***
20001215, by nipkow
'typedef': present result theorem "type_definition Rep Abs A";
20001214, by wenzelm
tuned;
20001214, by wenzelm
unsymbolize;
20001214, by wenzelm
use \<Sum> from main HOL;
20001214, by wenzelm
added Summation;
20001214, by wenzelm
many new proofs; still needs tidying
20001214, by paulson
new theorem real_lbound_gt_zero
20001214, by paulson
updated;
20001213, by wenzelm
eliminated GOAL syntax;
20001213, by wenzelm
fixed add_term_names: NameSpace.base;
20001213, by wenzelm
tuned comments;
20001213, by wenzelm
* print modes "brackets" and "no_brackets" control output of nested =>
20001213, by wenzelm
tidying
20001213, by paulson
new material, including default simprules that should be introduced earlier
20001213, by paulson
fixed iter_wf proof
20001213, by kleing
another round of tidyingup
20001213, by paulson
working proofs up to isCont_has_Ub
20001213, by paulson
tidying and replacement of "integer" rules by "order" ones
20001213, by paulson
removed sorry proof
20001213, by kleing
tries harder to remove negative literals, e.g.
20001213, by paulson
*** empty log message ***
20001213, by nipkow
*** empty log message ***
20001213, by nipkow
small mods.
20001213, by nipkow
sar split method uses new gen_split_tac.
20001213, by nipkow
completeness (unfinished)
20001212, by kleing
added direction dynamic ==> static
20001212, by kleing
less
more

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