command 'Isar.edit_document': actually invoke edit_document;

merged

fixed error message spacing

tuned interpretation code

tuned

type constraints and sort intersection

dropped $Id$

decativate Toplevel.debug after reading

exported break reference

tuned;

edit_document: proper edits/edit markup, including the document id; tuned;

replaced command_state by edits/edit;

removed junk;

merged

one more [code del] declaration

misc cleanup and simplification;

added run_command (from isar_document.ML); tuned;

added command_state markup;

tuned ASCII art;

declare pCons_0_0 [code post]

merged

code generation for polynomials

merged

more [code del] declarations

declare more definitions [code del]

define polynomial multiplication using poly_rec

merged.

declare smult rules [simp]

simplify proof of coeff_mult_degree_sum

convert Deriv.thy to use new Polynomial library (incomplete)

Integration imports ATP_Linkup (for metis)

misc internal rearrangements; fold_entries: really start from start, or optional position; added find_first_entries, find_first_entries; insert_entry: always invalidate next state; added refresh_states (partial version);

replaced sys_error by plain error; some basic operations on command entries within a document;

merged

change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)

convert Fundamental_Theorem_Algebra.thy to use new Polynomial library

add Polynomial.thy to makefile

add lemmas poly_power, poly_roots_finite

declare dvd_minus_iff and minus_dvd_iff [iff]

new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]

added Isar/isar_document.ML: Interactive Isar documents.

export list;

correctness and uniqueness of synthetic division

add synthetic division algorithm for polynomials

add list-style syntax for pCons

add recursion combinator poly_rec; define poly function using poly_rec

add lemmas degree_{add,diff}_less

merged

new theory of polynomials

tuned categories;

added outer_keyword.scala: Isar command keyword classification;

added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;

load main entry points sequentially, for reduced memory demands;

merged

merged

less ambitious ML_OPTIONS;

merged

merged

explicit bookkeeping of intro rules and axiom

stripped Id

construct explicit class morphism

less ambitious ML_OPTIONS;

schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;

future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;

added cancel_proofs, based on task groups of "entered" proofs;

added pending_groups -- accumulates task groups of local derivations only;

added cancel_group;

merged

schedule_futures: tuned final consolidation, explicit after_load phase;

load_thy: explicit after_load phase for presentation;

excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;

slightly more robust matching of session name;

merged

fixed proof involving dvd;

tuned;

added force_result;

use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;

simplified join_proofs;

merged

added split_thy_path;

added running task markup;

tuned;

merged

merged

merged.

fix proof broken by changes in dvd theory

merged.

remove type-specific proofs

add lemma dvd_diff to class comm_ring_1

add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1

move lemmas mult_minus{left,right} inside class ring

clean up division_ring proofs

add class ring_div; generalize mod/diff/minus proofs for class ring_div

generalize zmod_zmod_cancel -> mod_mod_cancel