wenzelm [Tue, 13 Jan 2009 22:20:49 +0100] rev 29468
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);
wenzelm [Tue, 13 Jan 2009 17:34:12 +0100] rev 29467
replaced sys_error by plain error;
some basic operations on command entries within a document;
wenzelm [Tue, 13 Jan 2009 14:31:02 +0100] rev 29466
merged
huffman [Mon, 12 Jan 2009 23:36:30 -0800] rev 29465
change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
huffman [Mon, 12 Jan 2009 22:41:08 -0800] rev 29464
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman [Mon, 12 Jan 2009 22:18:51 -0800] rev 29463
add Polynomial.thy to makefile
huffman [Mon, 12 Jan 2009 22:16:35 -0800] rev 29462
add lemmas poly_power, poly_roots_finite
huffman [Mon, 12 Jan 2009 12:10:41 -0800] rev 29461
declare dvd_minus_iff and minus_dvd_iff [iff]
huffman [Mon, 12 Jan 2009 12:09:54 -0800] rev 29460
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
wenzelm [Tue, 13 Jan 2009 13:47:35 +0100] rev 29459
added Isar/isar_document.ML: Interactive Isar documents.