Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
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.
removed dead code: listof;
20000505, by wenzelm
use Args.colon / Args.parens;
20000505, by wenzelm
adapted to new arithmetic simprocs;
20000505, by wenzelm
added scan_to_id (used to be in Pure/section_utils.ML);
20000505, by wenzelm
removed Pure/section_utils.ML;
20000505, by wenzelm
improved syntax of method options (no_asm) etc;
20000505, by wenzelm
removed index2;
20000505, by wenzelm
updated;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
GPLed;
20000505, by wenzelm
added simple_read_term;
20000505, by wenzelm
tuned msg;
20000505, by wenzelm
Added constant abs.
20000505, by nipkow
simprocs now simplify the RHS of their result
20000505, by paulson
new lemmas about binary division
20000505, by paulson
Added AVL
20000505, by nipkow
if_weak_cong should make linear arithmetic faster
20000504, by paulson
a safer way of proving literal equalities
20000504, by paulson
from Suc...Suc to #m
20000504, by paulson
of course it should use Main
20000504, by paulson
new lemmas concerning powers and #mmm
20000504, by paulson
changed 2 to #2
20000504, by paulson
Suc 0 > 1
20000504, by paulson
card_Pow is no longer a default simprule because it uses unary 2
20000504, by paulson
simprocs
20000504, by paulson
further tidying of integer simprocs
20000504, by paulson
removed obsolete simproc combine_coeff
20000503, by paulson
Installation of CombineNumerals for the integers
20000503, by paulson
removed obsolete simprocs
20000503, by paulson
removed obsolete "evenness" proofs
20000502, by paulson
TEMPORARY REMOVAL OF TWO BROKEN EXAMPLES
20000502, by paulson
modified for new simprocs
20000502, by paulson
now using binary naturals
20000502, by paulson
various bug fixes
20000502, by paulson
Cassini identity is easier to prove using INTEGERS
20000502, by paulson
a more modern proof
20000502, by paulson
now with combine_numerals
20000502, by paulson
combine_numerals replaces both fold_Suc and combine_coeff
20000502, by paulson
new simproc, replacing combine_coeffs and working for nat, int, real
20000502, by paulson
signature change
20000428, by paulson
inserted triviality check
20000428, by paulson
*** empty log message ***
20000425, by nipkow
new, but still slow, proofs using binary numerals
20000423, by paulson
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
20000423, by paulson
number_of now takes a type arg
20000423, by paulson
this change saves 15 seconds
20000423, by paulson
bug fixes to new simprocs
20000423, by paulson
[Int_CC.sum_conv, Int_CC.rel_conv] no longer exist
20000423, by paulson
removed some duplication, etc.
20000423, by paulson
now uses the new cancel_numerals simproc
20000423, by paulson
Provers/Arith/inverse_fold.ML is already obsolete
20000421, by paulson
cleaner exceptions
20000421, by paulson
now works for coefficients, not just for numerals
20000421, by paulson
new file containing simproc invocations, from NatBin.ML
20000421, by paulson
moved the simproc code to NatSimprocs.ML
20000421, by paulson
Provers/Arith/inverse_fold.ML is already obsolete
20000421, by paulson
less
more

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