huffman [Thu, 03 Jan 2008 22:09:44 +0100] rev 25814
new axclass finite_po < finite, po
huffman [Thu, 03 Jan 2008 22:08:54 +0100] rev 25813
add lub_maximal lemmas;
modify conclusion of directed_finiteD;
declare not_directed_empty [simp]
wenzelm [Thu, 03 Jan 2008 20:29:00 +0100] rev 25812
added class Property: basic Isabelle properties;
chaieb [Thu, 03 Jan 2008 18:19:27 +0100] rev 25811
tuned relevance test for presburger
wenzelm [Thu, 03 Jan 2008 17:50:44 +0100] rev 25810
output message properties: id or position;
wenzelm [Thu, 03 Jan 2008 17:50:43 +0100] rev 25809
toplevel print_exn: proper setmp_thread_properties;
wenzelm [Thu, 03 Jan 2008 17:50:42 +0100] rev 25808
added id property;
wenzelm [Thu, 03 Jan 2008 17:50:41 +0100] rev 25807
Result: added props field;
tuned;
huffman [Thu, 03 Jan 2008 17:22:24 +0100] rev 25806
remove legacy ML bindings
huffman [Thu, 03 Jan 2008 17:02:56 +0100] rev 25805
new-style theorem references
huffman [Thu, 03 Jan 2008 16:53:27 +0100] rev 25804
fix theorem references
huffman [Thu, 03 Jan 2008 16:31:53 +0100] rev 25803
generalized and simplified proof of adm_Finite
huffman [Thu, 03 Jan 2008 16:29:37 +0100] rev 25802
new lemma adm_upward
chaieb [Thu, 03 Jan 2008 10:27:40 +0100] rev 25801
Tuned (type information in Lemmas)
chaieb [Thu, 03 Jan 2008 10:27:34 +0100] rev 25800
Changed order of tactics in presburger --- thinning before case splits