isabelle: Changelog

krauss [Fri, 22 Jun 2007 10:23:37 +0200] rev 23473

new method "elim_to_cases" provides ad-hoc conversion of obtain-style elimination goals to a disjunction of existentials.

huffman [Thu, 21 Jun 2007 23:49:26 +0200] rev 23472

section headings

huffman [Thu, 21 Jun 2007 23:33:10 +0200] rev 23471

add thm antiquotations

huffman [Thu, 21 Jun 2007 23:28:44 +0200] rev 23470

spelling

huffman [Thu, 21 Jun 2007 22:52:22 +0200] rev 23469

add thm antiquotations

huffman [Thu, 21 Jun 2007 22:30:58 +0200] rev 23468

changed simp rules for of_nat

wenzelm [Thu, 21 Jun 2007 22:10:16 +0200] rev 23467

tuned proofs -- avoid implicit prems;

wenzelm [Thu, 21 Jun 2007 20:48:48 +0200] rev 23466

moved quantifier elimination tools to Tools/Qelim/;

wenzelm [Thu, 21 Jun 2007 20:48:47 +0200] rev 23465

moved Presburger setup back to Presburger.thy;

wenzelm [Thu, 21 Jun 2007 20:07:26 +0200] rev 23464

tuned proofs -- avoid implicit prems;

isabelle