updated;

eliminated GOAL syntax;

fixed add_term_names: NameSpace.base;

tuned comments;

* print modes "brackets" and "no_brackets" control output of nested => (types) and ==> (props); the default behaviour is "brackets";

tidying

new material, including default simprules that should be introduced earlier

fixed iter_wf proof

another round of tidying-up

working proofs up to isCont_has_Ub

tidying and replacement of "integer" rules by "order" ones

removed sorry proof

tries harder to remove negative literals, e.g. -2*x = 0 goes to x=0 rather than -x=0.

*** empty log message ***

*** empty log message ***

small mods.

sar split method uses new gen_split_tac.

completeness (unfinished)

added direction dynamic ==> static

eliminated some warnings, tuned

first stage in tidying up Real and Hyperreal. Factor cancellation simprocs inverse #0 = #0 simprules for division corrected ambigous syntax definitions in Hyperreal

deleting unused rules

greater use of overloaded rules (order_less_imp_le not zless_imp_zle, ...)

auto-updated

"translations": allow harpoons;

moved "_update_name" to HOL/Record;

tuned;

added "_update_name" and parse_translation;

alternative syntax for "translations": harpoons;

harpoons;