| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:52:31 +0100 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:40:05 +0200 |
paulson |
Tidied many proofs, using AddIffs to let equivalences take
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 15:29:05 +0200 |
paulson |
Removed the unused rel_eq_cs
|
file |
diff |
annotate
|
| Mon, 03 Jun 1996 17:10:56 +0200 |
berghofe |
best_tac, deepen_tac and safe_tac now also use default claset.
|
file |
diff |
annotate
|
| Thu, 23 May 1996 15:15:20 +0200 |
berghofe |
Removed equalityI from some proofs (because it is now included
|
file |
diff |
annotate
|
| Tue, 21 May 1996 13:39:31 +0200 |
berghofe |
Replaced fast_tac by Fast_tac (which uses default claset)
|
file |
diff |
annotate
|
| Sat, 27 Apr 1996 12:07:31 +0200 |
nipkow |
Added R_O_id and id_O_R
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 11:45:01 +0200 |
paulson |
Using new "Times" infix
|
file |
diff |
annotate
|
| Mon, 25 Mar 1996 11:13:59 +0100 |
nipkow |
added converse_converse
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 12:52:11 +0100 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 26 Jan 1996 20:25:39 +0100 |
nipkow |
Streamlined defs in Relation and added new intro/elim rules to do with
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:10:03 +0100 |
clasohm |
added local simpsets; removed IOA from 'make test'
|
file |
diff |
annotate
|
| Fri, 26 May 1995 18:11:47 +0200 |
nipkow |
Trancl is now based on Relation which used to be in Integ.
|
file |
diff |
annotate
|