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;

resolveq_cases_tac: insert facts;

added "consumes" attribute;

consume facts;

consumes0/1;

RuleCases.save;

*** empty log message ***

deleted unused result intrel_refl

*** empty log message ***

*** empty log message ***

*** empty log message ***

hide many names from Datatype_Universe.

exception Interrupt = SML90.Interrupt;

added exception Interrupt for use in function Library/try

arith_tac: atomize;

standard: close_derivation;

* HOL: syntax or "abs";

*** empty log message ***

tuned;

tuned;

*** empty log message ***

*** empty log message ***

tag result with name reference to final binding (basically just a comment);

Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;

replace \<dots>;

unsymbolize;

quote executable;

tuned;

;

adjusted for BV changes (Ok -> OK)