oheimb [Fri, 31 May 1996 20:14:42 +0200] rev 1780
adapted proof of flat_codom
oheimb [Fri, 31 May 1996 19:55:19 +0200] rev 1779
introduced forgotten bind_thm calls
oheimb [Fri, 31 May 1996 19:47:23 +0200] rev 1778
adapted some proofs for new simplifier
oheimb [Fri, 31 May 1996 19:34:40 +0200] rev 1777
renamed le_0 to le_0_eq, to avoid confusion with le0,
supplied an experimental thm Suc_le_eq, but commented it out
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.
nipkow [Fri, 24 May 1996 11:48:18 +0200] rev 1766
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
nipkow [Fri, 24 May 1996 11:46:40 +0200] rev 1765
Removed junk introduced by a cvs merge.
paulson [Fri, 24 May 1996 11:42:04 +0200] rev 1764
Augmented comment about conversion to clauses
berghofe [Thu, 23 May 1996 15:17:23 +0200] rev 1763
expanded TABs
berghofe [Thu, 23 May 1996 15:16:12 +0200] rev 1762
equalityI is now added to default claset
berghofe [Thu, 23 May 1996 15:15:20 +0200] rev 1761
Removed equalityI from some proofs (because it is now included
in the default claset)
berghofe [Thu, 23 May 1996 14:37:06 +0200] rev 1760
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
nipkow [Wed, 22 May 1996 18:32:37 +0200] rev 1759
Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
nipkow [Wed, 22 May 1996 17:30:16 +0200] rev 1758
Added ex_imp
nipkow [Wed, 22 May 1996 17:11:54 +0200] rev 1757
Added the second half of the W/I correspondence.
nipkow [Wed, 22 May 1996 16:54:16 +0200] rev 1756
Added swap_prems_rl
berghofe [Tue, 21 May 1996 13:42:53 +0200] rev 1755
Added additional parent theory equalities because some proofs in
Prod.ML depend on rules proved in equalities.ML
berghofe [Tue, 21 May 1996 13:39:31 +0200] rev 1754
Replaced fast_tac by Fast_tac (which uses default claset)
New rules are now also added to default claset.
nipkow [Tue, 21 May 1996 10:52:26 +0200] rev 1753
Corrected comment wrt I
nipkow [Tue, 21 May 1996 10:50:40 +0200] rev 1752
Updated url.
nipkow [Mon, 20 May 1996 18:41:55 +0200] rev 1751
Added thm I_complete_wrt_W to I.
Added a few lemmas to Maybe and Type.