| Wed, 02 Mar 1994 12:26:55 +0100 |
clasohm |
changed "." to "$" and Cons to infix "#" to eliminate ambiguity
|
changeset |
files
|
| Thu, 24 Feb 1994 14:45:57 +0100 |
nipkow |
typo in comment
|
changeset |
files
|
| Wed, 23 Feb 1994 10:05:35 +0100 |
nipkow |
some more sorting algorithms
|
changeset |
files
|
| Wed, 16 Feb 1994 15:13:53 +0100 |
nipkow |
added more lemmas (also to nat_ss)
|
changeset |
files
|
| Tue, 15 Feb 1994 10:05:17 +0100 |
nipkow |
deleted duplicate rewrite rules
|
changeset |
files
|
| Tue, 15 Feb 1994 07:55:22 +0100 |
nipkow |
added etac FalseE to the simplifier's solver.
|
changeset |
files
|
| Sat, 12 Feb 1994 14:46:21 +0100 |
nipkow |
added translations for "case xs of"
|
changeset |
files
|
| Fri, 11 Feb 1994 11:09:50 +0100 |
nipkow |
added ::bool in the defn of True.
|
changeset |
files
|
| Thu, 03 Feb 1994 09:55:47 +0100 |
nipkow |
Introduction of various new lemmas and of case_tac.
|
changeset |
files
|
| Thu, 27 Jan 1994 17:01:10 +0100 |
nipkow |
id -> idt in type of @filter and @Alls
|
changeset |
files
|
| Wed, 26 Jan 1994 17:53:27 +0100 |
nipkow |
sum: renamed case to sum_case
|
changeset |
files
|
| Mon, 24 Jan 1994 16:03:03 +0100 |
nipkow |
changed header
|
changeset |
files
|
| Mon, 24 Jan 1994 16:00:37 +0100 |
nipkow |
Verification of quicksort
|
changeset |
files
|
| Mon, 24 Jan 1994 15:59:44 +0100 |
nipkow |
added qsort
|
changeset |
files
|
| Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
changeset |
files
|
| Fri, 14 Jan 1994 12:35:27 +0100 |
lcp |
commented imageE
|
changeset |
files
|
| Fri, 07 Jan 1994 14:23:13 +0100 |
nipkow |
added let_weak_cong
|
changeset |
files
|
| Fri, 07 Jan 1994 14:22:37 +0100 |
nipkow |
added pair_eq
|
changeset |
files
|
| Wed, 05 Jan 1994 19:39:05 +0100 |
nipkow |
modified solver of HOL_ss to take the new simplifier into account: the thm to
|
changeset |
files
|
| Wed, 05 Jan 1994 19:37:07 +0100 |
nipkow |
added new rewrite rules to arith_ss
|
changeset |
files
|
| Tue, 04 Jan 1994 18:33:20 +0100 |
nipkow |
shortened use_thy section taking advantage of dependencies
|
changeset |
files
|
| Thu, 30 Dec 1993 10:19:44 +0100 |
nipkow |
added x ~: {} and x : insert(y,A) = ...
|
changeset |
files
|
| Wed, 22 Dec 1993 12:43:37 +0100 |
nipkow |
added Pair_eq to pair_ss in prod.ML
|
changeset |
files
|
| Tue, 14 Dec 1993 18:05:22 +0100 |
nipkow |
added syntax for nested lets.
|
changeset |
files
|
| Mon, 13 Dec 1993 18:43:03 +0100 |
lcp |
added mention of Subst
|
changeset |
files
|
| Fri, 03 Dec 1993 12:41:54 +0100 |
lcp |
added new example
Isabelle93
|
changeset |
files
|
| Wed, 01 Dec 1993 13:05:25 +0100 |
lcp |
HOL/llist/LList_corec_subset1: does not need induction
|
changeset |
files
|
| Tue, 30 Nov 1993 17:44:04 +0100 |
nipkow |
added pred: nat=>nat
|
changeset |
files
|
| Mon, 29 Nov 1993 18:35:02 +0100 |
nipkow |
changed simpsets
|
changeset |
files
|
| Thu, 25 Nov 1993 10:04:02 +0100 |
nipkow |
added "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"
|
changeset |
files
|