Tue, 13 Jan 2009 06:55:13 -0800 Integration imports ATP_Linkup (for metis)
huffman [Tue, 13 Jan 2009 06:55:13 -0800] rev 29469
Integration imports ATP_Linkup (for metis)
Tue, 13 Jan 2009 22:20:49 +0100 misc internal rearrangements;
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);
Tue, 13 Jan 2009 17:34:12 +0100 replaced sys_error by plain error;
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;
Tue, 13 Jan 2009 14:31:02 +0100 merged
wenzelm [Tue, 13 Jan 2009 14:31:02 +0100] rev 29466
merged
Mon, 12 Jan 2009 23:36:30 -0800 change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)
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)
Mon, 12 Jan 2009 22:41:08 -0800 convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
huffman [Mon, 12 Jan 2009 22:41:08 -0800] rev 29464
convert Fundamental_Theorem_Algebra.thy to use new Polynomial library
Mon, 12 Jan 2009 22:18:51 -0800 add Polynomial.thy to makefile
huffman [Mon, 12 Jan 2009 22:18:51 -0800] rev 29463
add Polynomial.thy to makefile
Mon, 12 Jan 2009 22:16:35 -0800 add lemmas poly_power, poly_roots_finite
huffman [Mon, 12 Jan 2009 22:16:35 -0800] rev 29462
add lemmas poly_power, poly_roots_finite
Mon, 12 Jan 2009 12:10:41 -0800 declare dvd_minus_iff and minus_dvd_iff [iff]
huffman [Mon, 12 Jan 2009 12:10:41 -0800] rev 29461
declare dvd_minus_iff and minus_dvd_iff [iff]
Mon, 12 Jan 2009 12:09:54 -0800 new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman [Mon, 12 Jan 2009 12:09:54 -0800] rev 29460
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip