Exported eval_wrapper.

- corrected bogus comment for function inst_conj_all - tuned function obtain_fresh_name

removed dead code

simplified prepare_command;

Isar.command: explicitly set transaction position, as required for prepare_command errors; adapted Isabelle.command;

Updated locale tests.

Generalised polynomial lemmas from cring to ring.

Removed import and lparams from locale record.

made setsum executable on int.

Tuned (for the sake of a meaningless log entry).

New locales for orders and lattices where the equivalence relation is not restricted to equality.

added hint about writing "x : set xs".

simple lifters

dropped imperative monad bind

facts_of

improved morphism

SML_imp, OCaml_imp

clarified

tuned

Zorn's Lemma for partial orders.

Definitions and some lemmas for reflexive orderings.

Lemmas added

New theory on divisibility.

Renamed theorems; New theory on divisibility.

New theorems on summation.

Unit_inv_l, Unit_inv_r made [simp].

New theory on divisibility; Restructured presentation.

Unit_inv_l, Unit_inv_r made [simp]; Renamed theorems; New theory on divisibility.

Haskell now living in the RealWorld

corrected Pure dependency

added removeAll

tuned; explicit export of element accessors

PureThy: dropped note_thmss_qualified, dropped _i suffix

some steps towards explicit class target for canonical interpretation

declare

*** empty log message ***

simplified a proof

tuned function name

tuned bootstrap order

subclass now also works for subclasses with empty specificaton

dropped PureThy.note; added PureThy.add_thm

added class preorder

dropped locale (open)

added explicit root theory; some tuning

tuned

dropped locale (open)

(re-)added simp rules for (_ + _) div/mod _

(re-)added simp rules for (_ + _) div/mod _

added explicit purge_data

added code generation

fixed code generator setup

(adjusted)

Tuned and corrected ideal_tac for algebra.

Theorems divides_le, ind_euclid, bezout_lemma, bezout_add, bezout, bezout_add_strong, gcd_unique,gcd_eq, bezout_gcd, bezout_gcd_strong, gcd_mult_distrib, gcd_bezout to GCD.thy

Tuned and simplified proofs; Rules added to presburger's and algebra's context; moved Bezout theorems from Primes.thy

Tuned and simplified proofs

Added theorems zmod_eq_dvd_iff and nat_mod_eq_iff previously in Pocklington.thy --- relevant for algebra

Relevant rules added to algebra's context

renamed item to span, renamed contructors; added span_range;

adapted ThyEdit.span;

maintain token range;

tty loop: do not report status;

added type range;

renamed command span markup;

SideKickParsedData: minimal content;

(adjusted)

(adjusted)

added verification framework for the HeapMonad and quicksort as example for this framework

build jedit plugin only if jedit is available;

misc tuning;

more class instantiations

refined code generator setup for rational numbers; more simplification rules for rational numbers

moved op dvd to theory Ring_and_Field; generalized a couple of lemmas

fixed Scala path;

tuned build order;

proper purge_tmp; remove .cvsignore files;

tuned message;

tuned line breaks (NB: generated text is inserted here);

proper usage message; more precise perl replacements; less verbosity;

make Isabelle source distribution (via Mercurial);

explicit Distribution.changelog;

structure Distribution: swapped default for is_official;

ThyInfo.remove_thy;

structure Distribution: swapped default for is_official; removed obsolete (?) sync/sleep;

use ../isabelle.sty and ../isabellesym.sty;

tuned whitespace;

removed old checklist;

obsolete;

tuned;

discontinued maketags;

assume GNU tar and find; Admin/build all; discontinued maketags;

tuned;

use ../isabellesym.sty, which is always available;

Admin/build browser;

less verbosity;

Administrative build -- finish Isabelle source distribution.

simplified proofs

beautified proofs

added lemmas

Added Standardization theory to nominal examples.

Added Standardization theory.

editor model: run interactively for now;

updated generated file;

identify: more informative id in Toplevel.debug mode; interactive state transformations: dispose descendants *before* running next command, bypass for control commands; editor model: actually run affected commands; misc tuning;

shortlogentry/filelogentry: show shortdate and full description;

Removed uses of context element includes.

added Isar.command, Isar.insert, Isar.remove (editor model);

export type id with no_id and create_command; basic support for editor model: insert_command, remove_command; refined command status; misc tuning;

tuned;

renamed IsarCmd.nested_command to OuterSyntax.prepare_command;

load thy_edit.ML before isar.ML;

modernized specifications and proofs; tuned document;

Removed uses of context element includes.

tuned

tuned code theorem bookkeeping

tuned changelogentry;

refined Output.status_fn: priority (only visible for non-empty output, e.g. via test_markup print mode);

support for command status;

added status channel; writeln_default: suppress empty messages;

added status channel;