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.
this makes the proof run (or run faster)
20001221, by paulson
further tidying of NSA proofs
20001221, by paulson
*** empty log message ***
20001221, by nipkow
rational arithmetic
20001221, by nipkow
rational arithemtic
20001221, by nipkow
reorientation of integer literals
20001221, by paulson
more tidying, especially to rationalize the simprules
20001221, by paulson
reorientation of 0=... (no idea why the backslashes have changed too)
20001221, by paulson
simproc bug fix: negative literals and large terms
20001221, by paulson
further tidying
20001220, by paulson
generalized the reorientation 0f 0=... to all types
20001220, by paulson
tidying, removing obsolete lemmas about 0=... and 1=...
20001220, by paulson
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
less
more

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