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)

thebibliography environment: replaced the Springer version by the standard one in book.cls

alternative function definition;

*** empty log message ***

BCV integration (type system is semilattice)

BCV integration (first step)

export freeze_thaw_type;

improved messages;

default_intro_classes_tac: Tactic.distinct_subgoals_tac;

axclass ordered_ring; instance int :: ordered_ring;

quot_cond_function: simplified, support conditional definition;

abs_eq_0: #0 instead of 0;

symbol syntax for "abs";

added axclass ordered_field;

check result: Envir.beta_norm;

Envir.beta_norm;

added beta_norm; tuned;

tuned;

removed quot_cond_function1, quot_function1; removed overloaded standard operations;

UNIV_witness;

Ring_and_Field;

Library/Ring_and_Field.thy;

rings and fields;

Proof.assert_forward;

added not_equiv_sym, not_equiv_trans1/2; tuned;

added abs_mult, abs_eq_0, square_nonzero;

ground terms section: new intro

CTT

separate rules for function/operation definitions;

renamed integ_le_less to int_le_less;

updated;

isabellebody: \par at begin/end;

auto update

first version of Advanced Inductive Defs section

x-symbol support for Pi, Sigma, -->, : (membership) note that "lam" is displayed as TWO lambda-symbols

new Main.thy as in HOL, ZF

added read_terms, read_props (simulataneous type-inference);

tuned statement args;

tuned IsarThy.theorem_i;

added students

Removed > and >=

Removed > and >= again.

quot_cond_definition;

simplified induction;

updated;

"induct" method: handle proper rules;

removed warning for "stripped" option;

removed junk;

Syntax.pure_appl_syntax declared as output syntax for theory ProtoPure;

* added overloaded operations "inverse" and "divide" (infix "/");

int_distrib;

nat_distrib;