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;