| 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
|
| Fri, 19 Nov 1993 11:36:23 +0100 |
lcp |
Trivial spacing corrections
|
changeset |
files
|
| Tue, 16 Nov 1993 14:14:22 +0100 |
clasohm |
changed use_thy's parameter to exact theory name
|
changeset |
files
|
| Tue, 09 Nov 1993 16:31:03 +0100 |
lcp |
Target "test" now depends on examples files
|
changeset |
files
|
| Tue, 09 Nov 1993 13:30:13 +0100 |
clasohm |
renamed meson-test.ML to mesontest.ML,
|
changeset |
files
|
| Tue, 09 Nov 1993 11:08:13 +0100 |
lcp |
co-induction example courtesy Jacob Frost
|
changeset |
files
|
| Wed, 03 Nov 1993 19:02:17 +0100 |
nipkow |
added append "@"
|
changeset |
files
|
| Mon, 25 Oct 1993 14:36:27 +0100 |
wenzelm |
added white-space;
|
changeset |
files
|
| Mon, 25 Oct 1993 14:35:17 +0100 |
wenzelm |
made ~= a fake infix;
|
changeset |
files
|
| Fri, 22 Oct 1993 13:36:28 +0100 |
clasohm |
changes for new Readthy
|
changeset |
files
|
| Sun, 17 Oct 1993 17:33:40 +0100 |
clasohm |
renamed: hol-rec.* to rec.*, lex-prod.* to lexprod.*, prop-log.* to pl.*
|
changeset |
files
|
| Sun, 17 Oct 1993 17:23:51 +0100 |
clasohm |
renamed utermlemmas.* to utlemmas.*
|
changeset |
files
|
| Fri, 08 Oct 1993 13:46:13 +0100 |
wenzelm |
removed THE;
|
changeset |
files
|
| Thu, 07 Oct 1993 10:29:23 +0100 |
lcp |
used ~= for "not equals" and ~: for "not in"
|
changeset |
files
|
| Thu, 07 Oct 1993 10:20:30 +0100 |
lcp |
added ~= for "not equals" and added ~: for "not in"
|
changeset |
files
|
| Mon, 04 Oct 1993 15:43:54 +0100 |
wenzelm |
HOL/hol.thy
|
changeset |
files
|
| Tue, 28 Sep 1993 14:27:31 +0100 |
lcp |
This repeats a previous commit, which failed to update simpdata.ML because
|
changeset |
files
|
| Wed, 22 Sep 1993 15:43:05 +0200 |
lcp |
Added weak congruence rules to HOL: if_weak_cong, case_weak_cong,
|
changeset |
files
|
| Thu, 16 Sep 1993 14:29:14 +0200 |
nipkow |
defined addcongs locally in simpdata.ML
|
changeset |
files
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
changeset |
files
|