oheimb [Fri, 31 May 1996 19:12:00 +0200] rev 1776
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
nipkow [Thu, 30 May 1996 13:31:29 +0200] rev 1775
Smaller logo
nipkow [Thu, 30 May 1996 13:29:52 +0200] rev 1774
Regrouped logo
nipkow [Wed, 29 May 1996 13:53:39 +0200] rev 1773
Added logo
nipkow [Wed, 29 May 1996 13:47:43 +0200] rev 1772
An Isabelle logo
nipkow [Wed, 29 May 1996 13:34:17 +0200] rev 1771
Replaced setsolver by addsolver
nipkow [Wed, 29 May 1996 12:03:32 +0200] rev 1770
Added addsolver
paulson [Tue, 28 May 1996 11:19:16 +0200] rev 1769
Simplified proof of deduction theorem
paulson [Tue, 28 May 1996 11:16:38 +0200] rev 1768
Corrected a comment in #34
berghofe [Fri, 24 May 1996 12:27:04 +0200] rev 1767
Rules pred_0, pred_Suc etc. are now stored in theorem database.