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

removed semicolons

rule subrelI (for nice Isar proofs of relation inequalities)

merged

merged

prefix normalizing replaces class_semiring

xsymbolized

moved method syntax here

tuned proof

former free-floating field_comp_conv now in structure Normalizer

proper sublocales; no free-floating ML sections

moved some lemmas from Groebner_Basis here

revert to loose merge semantics

merged

moved generic lemmas to appropriate places

tuned

dropped duplicate comp_arith

avoid open; tuned references to theorems

avoid references to groebner bases in names which have no references to groebner bases

tuned whitespace

tuned headings

avoid open

tuned internal structure

fail on merge of conflicting normalization entries: functions are not mergable

more canonical data administration

removed former algebra presimpset entirely

removed former algebra presimpset from accessor

removed former algebra presimpset from signature

moved presimplification rules for algebraic methods into named thms functor

tuned whitespace; dropped superfluous open

dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML

moved nat_arith ot Nat_Numeral: clarified normalizer setup

dropped unused file

dropped Id

remove unused constant preal_of_rat; remove several unused lemmas about preals

respectfullness and preservation of prod_rel

ProofContext.init_global

merged

farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)

constant name access lattice is not in use any longer

uniform treatment of length = 1 for forced breaks, also makes ML/Pretty.length coincide with Scala/XML.content_length;

replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;

added separate;

basic formatting of pretty trees; line-up ML vs. Scala sources;

added content_length;

slightly more general Library.chunks;

misc tuning -- accumulate body via ListBuffer;

basic support for symbolic pretty printing; tuned;

extractors for document updates; Session.handle_result: use extractors instead of raw patterns -- NB: using mixed patterns of case classes vs. extractors crashes Scala 2.8.1 RC1;

extractors for outer keyword declarations;

eliminated deprecated "--" method; use case classes with copy method for functional record update;

use IndexedSeq instead of deprecated RandomAccessSeq, which is merely an alias;

use SwingApplication instead of deprecated GUIApplication;

simplified via Position extractors;

some rearrangement of Scala sources;

fminus and some more theorems ported from Finite_Set.

eq_morphism is always optional: avoid trivial morphism for empty list of equations

tuned whitespace

tuned interpunctation, dropped dead comment

merged

avoid using '...' with LIMSEQ (cf. 1cc4ab4b7ff7)

generalize some lemmas to class t1_space