isabelle: Graph

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

put in some missing Hyperreal files
2001-01-01, by paulson
Hyperreal
2001-01-01, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-31, by paulson
now #16*(x+y) distributes for nat just as for other numeric types
2000-12-30, by paulson
a generic ordering theorem used in Real
2000-12-30, by paulson
tidying, and separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
separation of HOL-Hyperreal from HOL-Real
2000-12-30, by paulson
recover: ignore result;
2000-12-29, by wenzelm
recover: malformed result;
2000-12-29, by wenzelm
scan: malformed result;
2000-12-29, by wenzelm
recover: result;
2000-12-29, by wenzelm
proper error msg;
2000-12-29, by wenzelm
'erule' etc.: assm arg;
2000-12-27, by wenzelm
Method.erule 0;
2000-12-27, by wenzelm
updated;
2000-12-27, by wenzelm
'insert' made proper;
2000-12-27, by wenzelm
ares_tac, [edf]atac;
2000-12-27, by wenzelm
antiq: preview errors;
2000-12-23, by wenzelm
tuned length;
2000-12-23, by wenzelm
tuned output;
2000-12-23, by wenzelm
recover_order for single step tules;
2000-12-23, by wenzelm
simplified quick_and_dirty stuff;
2000-12-23, by wenzelm
tuned;
2000-12-23, by wenzelm
hide type node item;
2000-12-23, by wenzelm
Tools/string_syntax.ML;
2000-12-23, by wenzelm
tuned comment;
2000-12-23, by wenzelm
SML90 stuff;
2000-12-22, by wenzelm
handle proper rules;
2000-12-22, by wenzelm
export rewrite_cterm;
2000-12-22, by wenzelm
added inductive_conj;
2000-12-22, by wenzelm
tuned;
2000-12-22, by wenzelm
better definitions of SML90 features
2000-12-22, by paulson
*** empty log message ***
2000-12-21, by nipkow
something stopped working, had to add real_add_ac
2000-12-21, by nipkow
rational linear arithmetic
2000-12-21, by nipkow
this makes the proof run (or run faster)
2000-12-21, by paulson
further tidying of NSA proofs
2000-12-21, by paulson
*** empty log message ***
2000-12-21, by nipkow
rational arithmetic
2000-12-21, by nipkow
rational arithemtic
2000-12-21, by nipkow
re-orientation of integer literals
2000-12-21, by paulson
more tidying, especially to rationalize the simprules
2000-12-21, by paulson
re-orientation of 0=... (no idea why the backslashes have changed too)
2000-12-21, by paulson
simproc bug fix: negative literals and large terms
2000-12-21, by paulson
further tidying
2000-12-20, by paulson
generalized the re-orientation 0f 0=... to all types
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=... and 1=...
2000-12-20, by paulson
tidying, removing obsolete lemmas about 0=...
2000-12-20, by paulson
SML90: ord, chr, explode, implode;
2000-12-20, by wenzelm
re-orienting equations with #nnn on the lhs
2000-12-19, by paulson
re-orienting equations with 0, 1, 2 on the lhs
2000-12-19, by paulson
new file extract_common_term.ML for the cancel-factor simprocs
2000-12-19, by paulson
inserting the simproc nat_cancel_factor
2000-12-19, by paulson
inserting the simproc int_cancel_factor
2000-12-19, by paulson
new simprule zero_less_abs_iff
2000-12-19, by paulson
coping with the re-orientation of #nn=x
2000-12-19, by paulson
cancel-factor simproc allows shorter proofs
2000-12-19, by paulson
more tidying
2000-12-19, by paulson
cancel-factor simproc allows a shorter proof
2000-12-19, by paulson
improved errors;
2000-12-19, by wenzelm
*** empty log message ***
2000-12-18, by nipkow
*** empty log message ***
2000-12-18, by nipkow
new simproc for cancelling common factors, etc.
2000-12-18, by paulson
moved mk_bin from Numerals to HOLogic
2000-12-18, by nipkow
added rational arithmetic
2000-12-18, by nipkow
towards rtional arithmetic
2000-12-18, by nipkow
tidying and adding new proofs
2000-12-18, by paulson
loads the new simproc extract_common_term
2000-12-18, by paulson
'def': \<equiv>;
2000-12-16, by wenzelm
tuned HOL/Real/HahnBanach;
2000-12-16, by wenzelm
'def': equiv;
2000-12-16, by wenzelm
\isasymequiv;
2000-12-16, by wenzelm
updated;
2000-12-15, by wenzelm
corrected errors;
2000-12-15, by bauerg
usedir -m brackets;
2000-12-15, by wenzelm
GPLed;
2000-12-15, by wenzelm
tuned comment;
2000-12-15, by wenzelm
restore \int (integral);
2000-12-15, by wenzelm
tuned symbols;
2000-12-15, by wenzelm
further round of tidying
2000-12-15, by paulson
*** empty log message ***
2000-12-15, by nipkow
'typedef': present result theorem "type_definition Rep Abs A";
2000-12-14, by wenzelm
tuned;
2000-12-14, by wenzelm
unsymbolize;
2000-12-14, by wenzelm
use \<Sum> from main HOL;
2000-12-14, by wenzelm
added Summation;
2000-12-14, by wenzelm
many new proofs; still needs tidying
2000-12-14, by paulson
new theorem real_lbound_gt_zero
2000-12-14, by paulson
updated;
2000-12-13, by wenzelm
eliminated GOAL syntax;
2000-12-13, by wenzelm
fixed add_term_names: NameSpace.base;
2000-12-13, by wenzelm
tuned comments;
2000-12-13, by wenzelm
* print modes "brackets" and "no_brackets" control output of nested =>
2000-12-13, by wenzelm
tidying
2000-12-13, by paulson
new material, including default simprules that should be introduced earlier
2000-12-13, by paulson
fixed iter_wf proof
2000-12-13, by kleing
another round of tidying-up
2000-12-13, by paulson
working proofs up to isCont_has_Ub
2000-12-13, by paulson
tidying and replacement of "integer" rules by "order" ones
2000-12-13, by paulson
removed sorry proof
2000-12-13, by kleing
tries harder to remove negative literals, e.g.
2000-12-13, by paulson
*** empty log message ***
2000-12-13, by nipkow
*** empty log message ***
2000-12-13, by nipkow
small mods.
2000-12-13, by nipkow
sar split method uses new gen_split_tac.
2000-12-13, by nipkow
completeness (unfinished)
2000-12-12, by kleing
added direction dynamic ==> static
2000-12-12, by kleing
eliminated some warnings, tuned
2000-12-12, by kleing
first stage in tidying up Real and Hyperreal.
2000-12-12, by paulson
deleting unused rules
2000-12-12, by paulson
greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)
2000-12-12, by paulson
auto-updated
2000-12-12, by paulson
"translations": allow harpoons;
2000-12-11, by wenzelm
moved "_update_name" to HOL/Record;
2000-12-11, by wenzelm
tuned;
2000-12-11, by wenzelm
added "_update_name" and parse_translation;
2000-12-11, by wenzelm
alternative syntax for "translations": harpoons;
2000-12-11, by wenzelm
harpoons;
2000-12-11, by wenzelm
moved method lemma to BVSpec
2000-12-10, by kleing