isabelle: Changelog

wenzelm [Thu, 15 Dec 2005 19:42:03 +0100] rev 18415

improved proofs;

wenzelm [Thu, 15 Dec 2005 19:42:02 +0100] rev 18414

acc_induct: proper tags;

wenzelm [Thu, 15 Dec 2005 19:42:00 +0100] rev 18413

removed obsolete/unused setup_induction;

urbanc [Thu, 15 Dec 2005 18:13:40 +0100] rev 18412

tuned the proof of transitivity/narrowing

paulson [Thu, 15 Dec 2005 15:26:37 +0100] rev 18411

No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are deleted; any positive occurrence of HOL.type kills the entire clause.

urbanc [Thu, 15 Dec 2005 11:53:38 +0100] rev 18410

made further tunings

mengj [Thu, 15 Dec 2005 05:47:26 +0100] rev 18409

Added functions to test equivalence between clauses.

webertj [Wed, 14 Dec 2005 22:05:22 +0100] rev 18408

ex/Sudoku.thy

paulson [Wed, 14 Dec 2005 18:01:50 +0100] rev 18407

deleted redundant (looping!) simprule

paulson [Wed, 14 Dec 2005 16:14:41 +0100] rev 18406

modified example for new clauses

isabelle