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;

tuned;

simplified commit_exit;

simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;

removed obsolete commit_exit;

added command 'linear_undo'; tuned;

removed command 'redo'; added command 'linear_undo';

adapted ThyInfo.end_theory;

dropped map; fixed swap

curried gcd

cover macbroy as well; tuned;

tuned filelogentry;

print_mode "test_markup": do not change prompt, otherwise Proof General will not work;

tuned message;

updated generated file;

inform_file_processed: Isar.init_point last!

removed HOL-Complex, which has been discontinued after Isabelle2008;

added HOL-Nominal image;

removed obsolete Pure/General/history.ML;

inform_file_processed: try harder not to fail, ensure

commit_exit: proper error;

export EXCURSION_FAIL;

dropped junk

moved bootstrap of simplifier

tuned

end_theory: no result;

removed obsolete Toplevel.RESTART;

proper_inform_file_processed: new implementation based on global Isar state (cf. isar.ML); removed obsolete Toplevel.RESTART;

eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;

adapted IsarCmd.init_theory;

renamed theory to init_theory, removed obsolete kill argument; removed unused init_toplevel, begin_theory, end_theory; print_theorems: Toplevel.previous_node_of;

added commit_exit;

single_hyp(_meta)_subst_tac: Controlled substitution of a single hyp

renamed conversions to _conv, tuned

Simplified proofs

Simple theorems about zgcd moved to GCD.thy

Theorem names as in IntPrimes.thy, also several theorems moved from there

Fixed proofs.

ProofNode.current

command 'redo' no longer available;

replaced obsolete ProofHistory by ProofNode (backtracking only);

removed obsolete 'redo' command; cannot_undo: global history; tuned;

removed obsolete history commands; moved back, cannot_undo to isar_syn.ML;

Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).