clarified NEWS entry

merged

added NEWS entry

Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'

Add rules directly to the corresponding class locales instead.

Removed usage of normalizating locales.

speed up some proofs, fixing linarith_split_limit warnings

fix some linarith_split_limit warnings

include iszero_simps in semiring_norm just once (they are already included in rel_simps)

fix duplicate simp rule warning

no more RealPow.thy (remaining lemmas moved to RealDef.thy)

merged

simplify code for emptiness check

removed lemma real_sq_order; use power2_le_imp_le instead

merged

merged

represent de-Bruin indices simply by position in list

tuned reification functions

tuned code; toward a tightended interface with generated code

fix spelling of 'superseded'

NEWS: removed theory PReal

collected NEWS updates for HOLCF

merged

move floor lemmas from RealPow.thy to RComplete.thy

add lemma tendsto_Complex

move some theorems from RealPow.thy to Transcendental.thy

add lemma power2_eq_1_iff; generalize some other lemmas

minimize imports

move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff

clarified Pretty.font_metrics;

format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking;

tuned;

more precise pretty printing based on actual font metrics; removed obsolete relative margin;

predefined spaces;

merged

support Isabelle plugin properties with defaults; font size relative to view.textsize of jEdit; margin relative to component width and approximative font metrics;

merged

tuned proof so that no simplifier warning is printed

renamed former Int.int_induct to Int.int_of_nat_induct, former Presburger.int_induct to Int.int_induct: is more conservative and more natural than the intermediate solution

merged

tuned

theorem Presburger.int_induct has been renamed to Int.int_bidirectional_induct

tuned; dropped strange myassoc2

stylized COOPER exception

simplified oracle

shorten names

updated references to ML files

only one module fpr presburger method

moved int induction lemma to theory Int as int_bidirectional_induct

tuned theory text; dropped unused lemma

one structure is better than three

less complex organization of cooper source code

dropped unused bindings; avoid open (documents dependency on generated code more explicitly)

add real_mult_commute to legacy theorem names

new construction of real numbers using Cauchy sequences

add more credits to ex/Dedekind_Real.thy

put construction of reals using Dedekind cuts in HOL/ex

disable two stage save by default, to avoid change of file permissions (notably the dreaded executable bit on Cygwin);

simple dialogs: ensure Swing thread;

font size re-adjustment according to Lobo internals;

Scala for Netbeans 6.8v1.1.0rc2;

more convenient get_font;

renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;

more convenient look-and-feel setup;

more convenient get_font;

explicit getLines(n) ensures platform-independence -- our files follow the POSIX standard, not DOS;

updated to jedit 4.3.2;

ignore spurious TIMEOUT messages, maybe caused by change of actor semantics in scala-2.8;

adapted to scala-2.8.0.RC2;

merged

real_mult_commute -> mult_commute

avoid using real-specific versions of generic lemmas

avoid using real-specific versions of generic lemmas

remove a couple of redundant lemmas; simplify some proofs

merged

add lemmas one_less_inverse and one_le_inverse

do not redeclare [simp] rules, to avoid "duplicate rewrite rule" warnings

added lemmas rel_comp_UNION_distrib(2)

made SML/NJ happy;

reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;

Thm.unconstrainT based on Logic.unconstrainT -- no proofterm yet;

just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;

added Logic.unconstrain_allTs, based on calculations_for_thm_proof by krauss/schropp, but treat type variables uniformly as in strip_shyps (in thm.ML) or stripped_sorts (in more_thm.ML);

tuned;

removed unused "option" variants of "same" operations;

more basic replacement of newlines;

static Symbol.spaces;

proper use of var stopped;

removed junk;

tuned headers;

tuned;

merged

merged

moved normalization proof tool infrastructure to canonical algebraic classes

added lemmas

merged

renamed Normalizer to the more specific Semiring_Normalizer

delete Groebner_Basis directory -- only one file left

split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces

merged

moved lemma zdvd_period to theory Int

tuned;

discontinued Pretty.setdepth, which appears to be largely unused, but can disrupt important markup if enabled accidentally;

tuned error message: regular Pretty.string_of instead of raw Pretty.output;

unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;

renamed Thm.get_name -> Thm.derivation_name and Thm.put_name -> Thm.name_derivation, to emphasize the true nature of these operations;

prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";

tuned signature;

added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;

back-patching of axclass proofs;

back-patching via Single_Assignment.var;

support several sidekick parsers -- very basic default parser;

sidekick: unformatted content, notably without newlines;

unformatted output;

output symbolic pretty printing markup and format in the front end;

Pretty.formatted operates directly on XML trees, treating XML.Elem like a pro-forma block of indentation 0, like the ML version; tuned;

tuned;

strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;

use existing undefined function;

merged