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

generalize some div/mod lemmas; remove type-specific proofs

add tracing for domain package proofs

rename abbreviation square -> power2, to match theorem names

merged

split of Imperative_HOL theories from HOL-Library

NEWS and CONTRIBUTORS

dded code_thm antiquotation

made SML/NJ happy

merged

merged

tuned siganture of locale.ML

tuned signature; internal code reorganisation

tuned signature; changed locale predicate name convention

changed locale predicate name convention

inductive: added fork_mono flag;

added fork_mono flag, which is usually enabled in batch-mode only; mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;

Proof.global_future_terminal_proof;

Proof.global_future_proof;

future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;

more robust propagation of errors through bulk jobs;

qed/after_qed: singleton result;

Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;

future_terminal_proof: no fork for interactive mode, assert_backward;

added local_theory';

merged

proper local_theory after Class.class

more parallel loading;

more parallel loading;

merged

merged.

make cont_proc handle eta-contracted terms

implement is_closed_term using Term.loose_bvar

use Thm.close_derivation instead of standard

tuned;

merged

renamed structure ParList to Par_List;

parallelized merge_data;

tuned map: reduced overhead due to bulk jobs; tuned join_results: reduced overhead for finished futures; tuned;

added is_valid; added extend: support bulk jobs; tuned;

future_terminal_proof: check Future.enabled;

merged

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

removed locale adaption layer

rearranged target theories

removed locale adaption layer

merged

misc tuning and modernization;