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

simplify definition of t1_space; generalize lemma closed_sing and related lemmas

generalize some lemmas

convert comments to 'text' blocks

generalize more lemmas about limits

repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)

merged

generalize types of LIMSEQ and LIM; generalize many lemmas

make (f -- a --> x) an abbreviation for (f ---> x) (at a)

make (X ----> L) an abbreviation for (X ---> L) sequentially

adapt to removed premise on tendsto lemma (cf. 88f0125c3bd2)

declare cont_discrete_cpo [cont2cont]

remove unneeded constant Zseq

add lemmas eventually_nhds_metric and tendsto_mono

remove unneeded premise

add constants netmap and nhds

Merged.

Provide internal function for printing a single interpretation.

Explicitly manage export in dependencies.

fixed proof (cf. edc381bf7200);

Corrected imports; better approximation of dependencies.

Add Convex to Library build

Removed unnecessary assumption

Translating lemmas from Finite_Set to FSet.

merged

merged

Turned Sem into an inductive definition.

Corrected handling of "for" parameters.

induct_true_def and induct_false_def are already contained in induct_rulify_fallback.

added lemma about irreflexivity of pointer inequality in Imperative_HOL

added function ffilter and some lemmas from Finite_Set to the FSet theory

merged