2009-01-13 huffman 2009-01-13 declare smult rules [simp]
2009-01-13 huffman 2009-01-13 simplify proof of coeff_mult_degree_sum
2009-01-13 huffman 2009-01-13 convert Deriv.thy to use new Polynomial library (incomplete)
2009-01-13 huffman 2009-01-13 Integration imports ATP_Linkup (for metis)
2009-01-13 wenzelm 2009-01-13 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);
2009-01-13 wenzelm 2009-01-13 replaced sys_error by plain error; some basic operations on command entries within a document;
2009-01-13 wenzelm 2009-01-13 merged
2009-01-12 huffman 2009-01-12 change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
2009-01-12 huffman 2009-01-12 convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
2009-01-12 huffman 2009-01-12 add Polynomial.thy to makefile
2009-01-12 huffman 2009-01-12 add lemmas poly_power, poly_roots_finite
2009-01-12 huffman 2009-01-12 declare dvd_minus_iff and minus_dvd_iff [iff]
2009-01-12 huffman 2009-01-12 new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
2009-01-13 wenzelm 2009-01-13 added Isar/isar_document.ML: Interactive Isar documents.
2009-01-13 wenzelm 2009-01-13 export list;
2009-01-12 huffman 2009-01-12 correctness and uniqueness of synthetic division
2009-01-12 huffman 2009-01-12 add synthetic division algorithm for polynomials
2009-01-12 huffman 2009-01-12 add list-style syntax for pCons
2009-01-12 huffman 2009-01-12 add recursion combinator poly_rec; define poly function using poly_rec
2009-01-12 huffman 2009-01-12 add lemmas degree_{add,diff}_less
2009-01-11 wenzelm 2009-01-11 merged
2009-01-11 huffman 2009-01-11 new theory of polynomials
2009-01-11 wenzelm 2009-01-11 tuned categories;
2009-01-11 wenzelm 2009-01-11 added outer_keyword.scala: Isar command keyword classification;
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-11 wenzelm 2009-01-11 load main entry points sequentially, for reduced memory demands;
2009-01-11 wenzelm 2009-01-11 merged
2009-01-11 wenzelm 2009-01-11 merged
2009-01-11 wenzelm 2009-01-11 less ambitious ML_OPTIONS;
2009-01-11 wenzelm 2009-01-11 merged
2009-01-11 haftmann 2009-01-11 merged
2009-01-11 haftmann 2009-01-11 explicit bookkeeping of intro rules and axiom
2009-01-11 haftmann 2009-01-11 stripped Id
2009-01-11 haftmann 2009-01-11 construct explicit class morphism
2009-01-11 wenzelm 2009-01-11 less ambitious ML_OPTIONS;
2009-01-10 wenzelm 2009-01-10 schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;
2009-01-10 wenzelm 2009-01-10 future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10 wenzelm 2009-01-10 remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;
2009-01-10 wenzelm 2009-01-10 added cancel_proofs, based on task groups of "entered" proofs;
2009-01-10 wenzelm 2009-01-10 added pending_groups -- accumulates task groups of local derivations only;
2009-01-10 wenzelm 2009-01-10 added cancel_group;
2009-01-10 wenzelm 2009-01-10 merged
2009-01-10 wenzelm 2009-01-10 schedule_futures: tuned final consolidation, explicit after_load phase;
2009-01-10 wenzelm 2009-01-10 load_thy: explicit after_load phase for presentation;
2009-01-10 wenzelm 2009-01-10 excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;
2009-01-10 wenzelm 2009-01-10 slightly more robust matching of session name;
2009-01-10 wenzelm 2009-01-10 merged
2009-01-10 wenzelm 2009-01-10 fixed proof involving dvd;
2009-01-10 wenzelm 2009-01-10 tuned;
2009-01-10 wenzelm 2009-01-10 added force_result;
2009-01-10 wenzelm 2009-01-10 use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;
2009-01-10 wenzelm 2009-01-10 simplified join_proofs;
2009-01-09 wenzelm 2009-01-09 merged
2009-01-09 wenzelm 2009-01-09 added split_thy_path;
2009-01-09 wenzelm 2009-01-09 added running task markup;
2009-01-08 wenzelm 2009-01-08 tuned;
2009-01-08 wenzelm 2009-01-08 merged
2009-01-09 wenzelm 2009-01-09 merged
2009-01-09 huffman 2009-01-09 merged.