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;

moved method lemma to BVSpec

kildall ==> wt_method for whole program

tuned;

unsymbolize;

tuned;

Id;

generate table of isabelle symbols;

removed Digest (temporarily, not up to date) added theory JVM

updated for is_class changes

removed two intermediate comments

fixed and cleaned up wt[l]_jvm_prog proofs

tuned;

update for changes in Correct.thy and class/is_class defs

strengthened invariant: current class must be defined

update for changes in Step.thy

invoked class must be defined in Invoke C ...

unsymbolize;

left_minus axiom;

tuned;

activate Rational_Numbers;

deactivate Rational_Numbers (tmp!);

updated;

Rational_Numbers;

less rude treatment of "no_def";

added Library/Rational_Numbers.thy;

improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" cleanup of many proofs, removed superfluous tactics and theorems

improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO:

simplified interactive handling

some derived properties;

HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse" function;

*** empty log message ***

converted rinv and hrinv to inverse;

converted rinv to inverse;

added \<a> ... \<z>;

tuned;

theory file for Numbers section

auto generated

auto update

deleting the assumption 0<c for div_mult2_eq and mod_mult2_eq and simplifying their proofs

miniscoping of nat_diff_split

new theory Numbers.thy

new package amsfonts

tidying

partial numerics section

nat and int sections but no real

fixed document preparation

BCV Integration

jvm_progs now also store maximum op_stack depth

*** empty log message ***

*** empty log message ***

updated;

proper order of symbols for genarated table in system manual;

added \isabeginpar, \isaendpar;

proper order of modes;

diagnostic commands: comment;

export get_skolem;

fixed binding of parameters;

dignostic commands: comment;

include table of Isabelle standard symbols;

loads the new theory Numbers.thy

fixed formatting in section heading

auto update

tuned;

Now adjusted to mixed terms involving coercions.

Linear arithmetic now copes with mixed nat/int formulae.

append print modes;

no_brackets mode;

use_dir: modes;

append print_modes;

ignore quick_and_dirty for coind;

FreeUltrafilterNat ("\\<U>");

schematic goals;

removed quick_and_dirty;

superscripts: syntax (latex);

usedir: -m option;

added \mathcal A-Z;

option -m;

*** empty log message ***

*** empty log message ***

many new div and mod properties (borrowed from Integ/IntDiv)

renamed less_eq_Suc_add to less_imp_Suc_add

tuned;

removed "./configure";

/usr/bin/env bash;

schematic props;

removed get_goal; suffer schematic (top-level) goals;

added is_replaced_dummy_pattern;

renamed "equivalence_class" to "class";

schematic goals;

cases/induct: tuned handling of facts ('consumes');

'consumes' att;

misc;

replaced Eps by SOME

*** empty log message ***

some properties;

*** empty log message ***

resolveq_cases_tac moved here from Pure/Isar/method.ML; induct: proper handling of non-consumed facts;

resolveq(_cases)_tac moved to HOL/Tools/induct_method.ML;

expand_split_asm -> split_split_asm

*** empty log message ***

*** empty log message ***

simproc for cancelling common factors around = < <= div /

invoking CancelNumeralFactorFun

new simproc file cancel_numeral_factor.ML

added a reference to {sec:products} for ordered pair reasoning

fixed hostname;

detect CVSROOT;

tuned;

added consumes, consumes_default; added save; tuned;