| Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 16:33:28 +0200 |
nipkow |
moved inj and surj from Set to Fun and Inv -> inv.
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Thu, 03 Apr 1997 10:29:57 +0200 |
paulson |
Declares overloading for set-theoretic constants
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 11:25:04 +0200 |
paulson |
Re-ordering of rules to assist blast_tac
|
file |
diff |
annotate
|
| Wed, 05 Mar 1997 09:59:55 +0100 |
paulson |
New version of InterE, like its ZF counterpart
|
file |
diff |
annotate
|
| Wed, 12 Feb 1997 18:53:59 +0100 |
nipkow |
New class "order" and accompanying changes.
|
file |
diff |
annotate
|
| Thu, 09 Jan 1997 10:23:39 +0100 |
paulson |
Tidying of proofs. New theorems are enterred immediately into the
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 25 Sep 1996 11:14:18 +0200 |
paulson |
Rationalized the rewriting of membership for {} and insert
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:40:05 +0200 |
paulson |
Tidied many proofs, using AddIffs to let equivalences take
|
file |
diff |
annotate
|
| Thu, 22 Aug 1996 12:24:58 +0200 |
paulson |
Proved mem_if
|
file |
diff |
annotate
|
| Mon, 19 Aug 1996 11:51:39 +0200 |
paulson |
Added impOfSubs
|
file |
diff |
annotate
|
| Fri, 26 Jul 1996 12:16:17 +0200 |
paulson |
Proved bex_False
|
file |
diff |
annotate
|
| Fri, 28 Jun 1996 15:28:29 +0200 |
paulson |
Added contra_subsetD and rev_contra_subsetD
|
file |
diff |
annotate
|
| Tue, 18 Jun 1996 16:38:48 +0200 |
paulson |
New rewrites for vacuous quantification
|
file |
diff |
annotate
|
| Fri, 31 May 1996 19:12:00 +0200 |
oheimb |
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
|
file |
diff |
annotate
|
| Thu, 23 May 1996 15:16:12 +0200 |
berghofe |
equalityI is now added to default claset
|
file |
diff |
annotate
|
| Thu, 23 May 1996 14:37:06 +0200 |
berghofe |
Replaced fast_tac by Fast_tac (which uses default claset)
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 11:41:35 +0200 |
paulson |
Added more _iff rewrites for Compl, Un, Int
|
file |
diff |
annotate
|
| Wed, 27 Mar 1996 18:45:17 +0100 |
paulson |
Library changes for mutilated checkerboard
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 12:52:11 +0100 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 10:05:00 +0100 |
nipkow |
Added 'section' commands
|
file |
diff |
annotate
|
| Mon, 04 Mar 1996 14:37:33 +0100 |
nipkow |
Added a constant UNIV == {x.True}
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|