Fri, 31 May 1996 20:25:59 +0200 adapted use of monofun_cfun_arg
oheimb [Fri, 31 May 1996 20:25:59 +0200] rev 1781
adapted use of monofun_cfun_arg
Fri, 31 May 1996 20:14:42 +0200 adapted proof of flat_codom
oheimb [Fri, 31 May 1996 20:14:42 +0200] rev 1780
adapted proof of flat_codom
Fri, 31 May 1996 19:55:19 +0200 introduced forgotten bind_thm calls
oheimb [Fri, 31 May 1996 19:55:19 +0200] rev 1779
introduced forgotten bind_thm calls
Fri, 31 May 1996 19:47:23 +0200 adapted some proofs for new simplifier
oheimb [Fri, 31 May 1996 19:47:23 +0200] rev 1778
adapted some proofs for new simplifier
Fri, 31 May 1996 19:34:40 +0200 renamed le_0 to le_0_eq, to avoid confusion with le0,
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
Fri, 31 May 1996 19:12:00 +0200 moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
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
Thu, 30 May 1996 13:31:29 +0200 Smaller logo
nipkow [Thu, 30 May 1996 13:31:29 +0200] rev 1775
Smaller logo
Thu, 30 May 1996 13:29:52 +0200 Regrouped logo
nipkow [Thu, 30 May 1996 13:29:52 +0200] rev 1774
Regrouped logo
Wed, 29 May 1996 13:53:39 +0200 Added logo
nipkow [Wed, 29 May 1996 13:53:39 +0200] rev 1773
Added logo
Wed, 29 May 1996 13:47:43 +0200 An Isabelle logo
nipkow [Wed, 29 May 1996 13:47:43 +0200] rev 1772
An Isabelle logo
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip