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.
More deterministic (?) contr_tac
19971212, by paulson
More deterministic and therefore faster (sometimes) proof reconstruction
19971212, by paulson
ugly patch for new Blast_tac
19971212, by paulson
Faster proof of mult_less_cancel2
19971212, by paulson
tuned;
19971211, by wenzelm
Tidied final proof
19971211, by paulson
Tidied proof of finite_subset_induct
19971211, by paulson
Got rid of mod2_neq_0
19971211, by paulson
\subsection{*Theory inclusion};
19971208, by wenzelm
Tidying to fix overfull lines, etc
19971208, by paulson
Comprehensive (??) list of bugs, fixed or not
19971208, by paulson
tuned;
19971207, by wenzelm
added print_claset;
19971207, by wenzelm
Replaced Fib(Suc n)~=0 by 0<Fib(Suc(n)).
19971206, by nipkow
Got rid of some preds and replaced some n~=0 by 0<n.
19971206, by nipkow
Cleaned up arithmetic mess.
19971206, by nipkow
instantiate';
19971205, by wenzelm
changed typed_print_translation;
19971205, by wenzelm
tuned;
19971205, by wenzelm
nat_cancel enabled by default;
19971205, by wenzelm
adapted proofs to cope with simprocs nat_cancel;
19971205, by wenzelm
improved arbitrary_def: we now really don't know nothing about it!
19971205, by wenzelm
use_thy no longer requires writable current directory;
19971205, by wenzelm
adapted proofs to cope with simprocs nat_cancel (by Stefan Berghofer);
19971205, by wenzelm
simplification procedures nat_cancel enabled by default;
19971205, by wenzelm
tmp_name;
19971205, by wenzelm
added print_simpset;
19971204, by wenzelm
added is_base;
19971204, by wenzelm
added reset_context;
19971204, by wenzelm
added eq_set;
19971204, by wenzelm
moved global_names ref to Pure/ROOT.ML;
19971204, by wenzelm
pred > 1
19971204, by nipkow
pred n > n1
19971204, by nipkow
Simplified proofs.
19971204, by nipkow
Added thm mult_div_cancel
19971204, by nipkow
n ~= 0 should become 0 < n
19971203, by nipkow
Replaced n ~= 0 by 0 < n
19971203, by nipkow
pass return code!!
19971203, by wenzelm
Fixed the treatment of substitution for equations, restricting occurrences of
19971203, by paulson
updated for latest Blast_tac, which treats equality differently
19971203, by paulson
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
19971203, by paulson
Tidying and some comments
19971203, by paulson
updated for latest Blast_tac, which treats equality differently
19971203, by paulson
Instantiated the onepointrule quantifier simpprocs for FOL
19971203, by paulson
updated for latest Blast_tac, which fixes an equality bug
19971203, by paulson
Miniscoping now used except for one proof
19971203, by paulson
adapted to new term order;
19971202, by wenzelm
tuned term order;
19971202, by wenzelm
tuned trfuns types;
19971202, by wenzelm
added prod_ord, dict_ord, list_ord;
19971202, by wenzelm
File.tmp_name;
19971202, by wenzelm
added tmp_name;
19971202, by wenzelm
ISABELLE_TMP;
19971202, by wenzelm
added context.ML;
19971202, by wenzelm
Global contexts: session and theory.
19971202, by wenzelm
added Thy/context.ML;
19971202, by wenzelm
open;
19971201, by wenzelm
nat_cancel simprocs;
19971201, by wenzelm
ISABELLE_TMP_PREFIX;
19971201, by wenzelm
ISABELLE_TMP;
19971201, by wenzelm
less
more

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