| Mon, 09 Sep 1996 10:59:32 +0200 |
paulson |
Removal of (EX x. P) <-> P and (ALL x. P) <-> P
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 18:28:01 +0200 |
paulson |
Introduction of miniscoping for FOL
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:20:37 +0200 |
paulson |
Added a lot of basic laws, from HOL/simpdata
|
file |
diff |
annotate
|
| Mon, 06 May 1996 15:21:05 +0200 |
berghofe |
Added split_inside_tac.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:58:15 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 03 May 1995 13:35:09 +0200 |
lcp |
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
|
file |
diff |
annotate
|
| Thu, 30 Mar 1995 13:36:00 +0200 |
lcp |
Defined addss to perform simplification in a claset.
|
file |
diff |
annotate
|
| Wed, 08 Mar 1995 14:01:08 +0100 |
nipkow |
Enforced partial evaluation of mk_case_split_tac.
|
file |
diff |
annotate
|
| Wed, 14 Dec 1994 16:48:36 +0100 |
lcp |
conj_commute,disj_commute: new
|
file |
diff |
annotate
|
| Wed, 30 Nov 1994 13:18:42 +0100 |
clasohm |
added qed_goal for meta_iffD
|
file |
diff |
annotate
|
| Fri, 25 Nov 1994 00:02:37 +0100 |
lcp |
added blank line
|
file |
diff |
annotate
|
| Fri, 17 Jun 1994 17:49:03 +0200 |
lcp |
atomize: borrowed HOL version, which checks for both Trueprop
|
file |
diff |
annotate
|
| Tue, 24 May 1994 09:04:03 +0200 |
nipkow |
Modified mk_meta_eq to leave meta-equlities on unchanged.
|
file |
diff |
annotate
|
| Fri, 13 May 1994 11:25:55 +0200 |
lcp |
FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
|
file |
diff |
annotate
|
| Thu, 17 Mar 1994 13:54:50 +0100 |
lcp |
FOL/simpdata: tidied
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:41:37 +0100 |
nipkow |
updated solver of FOL_ss. see change of HOL/simpdata.ML
|
file |
diff |
annotate
|
| Tue, 12 Oct 1993 13:39:35 +0100 |
nipkow |
Added gen_all to simpdata.ML.
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 16:55:17 +0200 |
nipkow |
defined local addcongs
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|