| Thu, 29 Jun 1995 12:29:58 +0200 |
clasohm |
changed HOL to Old_HOL
Isabelle94-4
|
file |
diff |
annotate
|
| Thu, 06 Apr 1995 11:18:02 +0200 |
lcp |
Added Id: line
|
file |
diff |
annotate
|
| Wed, 15 Mar 1995 10:44:26 +0100 |
lcp |
Now calls exit_use instead of use, for prompt failure if errors are detected.
|
file |
diff |
annotate
|
| Wed, 08 Mar 1995 17:22:28 +0100 |
nipkow |
Added dependencies on ../Provers/hypsubst.ML and removed those on
|
file |
diff |
annotate
|
| Tue, 28 Feb 1995 10:48:46 +0100 |
lcp |
Re-organised to perform the tests independently. Now test
|
file |
diff |
annotate
|
| Fri, 03 Feb 1995 16:21:45 +0100 |
nipkow |
Add dependence on ex/String.thy/ML
|
file |
diff |
annotate
|
| Thu, 01 Dec 1994 17:35:03 +0100 |
nipkow |
Added dependency on thy_syntax.ML
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 20:07:22 +0100 |
nipkow |
added IMP/Properties
|
file |
diff |
annotate
|
| Thu, 24 Nov 1994 20:00:52 +0100 |
nipkow |
Trancl.{thy,ML} was missing
|
file |
diff |
annotate
|
| Fri, 11 Nov 1994 10:35:03 +0100 |
lcp |
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
|
file |
diff |
annotate
|
| Sun, 06 Nov 1994 21:04:39 +0100 |
clasohm |
changed command for making 'test'
|
file |
diff |
annotate
|
| Wed, 02 Nov 1994 15:26:13 +0100 |
clasohm |
added IOA files
|
file |
diff |
annotate
|
| Wed, 28 Sep 1994 12:39:32 +0100 |
nipkow |
moved LList* to ex
|
file |
diff |
annotate
|
| Wed, 31 Aug 1994 17:50:59 +0200 |
nipkow |
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
|
file |
diff |
annotate
|
| Tue, 30 Aug 1994 10:04:49 +0200 |
nipkow |
New version of datatype.ML with primrec (Norbert).
|
file |
diff |
annotate
|
| Thu, 25 Aug 1994 11:01:45 +0200 |
lcp |
INSTALLATION OF INDUCTIVE DEFINITIONS
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 11:25:16 +0200 |
lcp |
HOL/Makefile, ROOT: updated for new .thy files
|
file |
diff |
annotate
|
| Thu, 21 Jul 1994 10:52:00 +0200 |
lcp |
HOL/Makefile: now test depends upon SUBST_FILES
|
file |
diff |
annotate
|
| Wed, 01 Jun 1994 13:24:54 +0200 |
lcp |
added test for $ISABELLEBIN=source directory, to
|
file |
diff |
annotate
|
| Sun, 24 Apr 1994 11:27:38 +0200 |
clasohm |
renamed theory files
isa94
|
file |
diff |
annotate
|
| Fri, 22 Apr 1994 21:23:14 +0200 |
clasohm |
renamed theory files
|
file |
diff |
annotate
|
| Tue, 22 Mar 1994 18:07:45 +0100 |
nipkow |
added dependency on datatype.ML
|
file |
diff |
annotate
|
| Mon, 24 Jan 1994 15:59:02 +0100 |
nipkow |
added conj_assoc to HOL_ss
|
file |
diff |
annotate
|
| Tue, 09 Nov 1993 16:31:03 +0100 |
lcp |
Target "test" now depends on examples files
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:21:07 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|