isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

Simplified proofs.
1997-12-04, by nipkow
Added thm mult_div_cancel
1997-12-04, by nipkow
n ~= 0 should become 0 < n
1997-12-03, by nipkow
Replaced n ~= 0 by 0 < n
1997-12-03, by nipkow
pass return code!!
1997-12-03, by wenzelm
Fixed the treatment of substitution for equations, restricting occurrences of
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Moved some functions from ZF/ind_syntax.ML to FOL/fologic.ML
1997-12-03, by paulson
Tidying and some comments
1997-12-03, by paulson
updated for latest Blast_tac, which treats equality differently
1997-12-03, by paulson
Instantiated the one-point-rule quantifier simpprocs for FOL
1997-12-03, by paulson
updated for latest Blast_tac, which fixes an equality bug
1997-12-03, by paulson
Miniscoping now used except for one proof
1997-12-03, by paulson
adapted to new term order;
1997-12-02, by wenzelm
tuned term order;
1997-12-02, by wenzelm
tuned trfuns types;
1997-12-02, by wenzelm
added prod_ord, dict_ord, list_ord;
1997-12-02, by wenzelm
File.tmp_name;
1997-12-02, by wenzelm
added tmp_name;
1997-12-02, by wenzelm
ISABELLE_TMP;
1997-12-02, by wenzelm
added context.ML;
1997-12-02, by wenzelm
Global contexts: session and theory.
1997-12-02, by wenzelm
added Thy/context.ML;
1997-12-02, by wenzelm
open;
1997-12-01, by wenzelm
nat_cancel simprocs;
1997-12-01, by wenzelm
ISABELLE_TMP_PREFIX;
1997-12-01, by wenzelm
ISABELLE_TMP;
1997-12-01, by wenzelm
Added DiffCancelSums.
1997-12-01, by berghofe
New guarantee B_trusts_NS5, and tidying
1997-12-01, by paulson
speed-up
1997-12-01, by paulson

less more | (0) -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle