nipkow [Mon, 24 Jan 1994 15:59:44 +0100] rev 35
added qsort
nipkow [Mon, 24 Jan 1994 15:59:02 +0100] rev 34
added conj_assoc to HOL_ss
added filter, mem, and some syntax to lists
lcp [Fri, 14 Jan 1994 12:35:27 +0100] rev 33
commented imageE
nipkow [Fri, 07 Jan 1994 14:23:13 +0100] rev 32
added let_weak_cong
nipkow [Fri, 07 Jan 1994 14:22:37 +0100] rev 31
added pair_eq
nipkow [Wed, 05 Jan 1994 19:39:05 +0100] rev 30
modified solver of HOL_ss to take the new simplifier into account: the thm to
be solved may have assumption.
nipkow [Wed, 05 Jan 1994 19:37:07 +0100] rev 29
added new rewrite rules to arith_ss
nipkow [Tue, 04 Jan 1994 18:33:20 +0100] rev 28
shortened use_thy section taking advantage of dependencies
nipkow [Thu, 30 Dec 1993 10:19:44 +0100] rev 27
added x ~: {} and x : insert(y,A) = ...
nipkow [Wed, 22 Dec 1993 12:43:37 +0100] rev 26
added Pair_eq to pair_ss in prod.ML
removed it locally in llist.ML because preconditions of the form <a,b> =
<?x,?y>, which used to be solved by reflexivity, now rewrote to a = ?x & b =
?y, which is not solved by reflexivity.