| Wed, 03 Oct 2001 20:54:16 +0200 |
wenzelm |
tuned parentheses in relational expressions;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Thu, 15 Feb 2001 16:00:40 +0100 |
oheimb |
moved inv_image to Relation
|
file |
diff |
annotate
|
| Tue, 09 Jan 2001 15:22:13 +0100 |
nipkow |
`` -> and ``` -> ``
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 18:48:18 +0100 |
nipkow |
^^ -> ```
|
file |
diff |
annotate
|
| Fri, 05 Jan 2001 10:19:14 +0100 |
paulson |
Field of a relation, and some Domain/Range rules
|
file |
diff |
annotate
|
| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Fri, 23 Jun 2000 10:43:43 +0200 |
paulson |
new theorem trans_O_subset
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Wed, 21 Jun 2000 10:31:34 +0200 |
paulson |
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:01:50 +0200 |
nipkow |
Times -> <*>
|
file |
diff |
annotate
|
| Mon, 21 Feb 2000 13:57:07 +0100 |
oheimb |
renamed Univalent to univalent
|
file |
diff |
annotate
|
| Mon, 21 Feb 2000 10:20:38 +0100 |
nipkow |
A few lemmas and some Adds.
|
file |
diff |
annotate
|
| Mon, 31 Jan 2000 16:18:42 +0100 |
paulson |
new theorem rev_ImageI
|
file |
diff |
annotate
|
| Thu, 11 Nov 1999 10:24:14 +0100 |
paulson |
Fixed obsolete use of "op ^^"; new lemma
|
file |
diff |
annotate
|
| Fri, 22 Oct 1999 18:26:46 +0200 |
paulson |
new theorems on Image
|
file |
diff |
annotate
|
| Mon, 11 Oct 1999 10:49:18 +0200 |
paulson |
new thm Domain_mono
|
file |
diff |
annotate
|
| Mon, 26 Jul 1999 16:29:38 +0200 |
paulson |
three new theorems
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:24:35 +0200 |
paulson |
getting rid of qed_goal
|
file |
diff |
annotate
|
| Fri, 16 Jul 1999 12:09:48 +0200 |
berghofe |
Added some definitions and theorems needed for the
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:27:54 +0200 |
paulson |
qed_goal -> Goal
|
file |
diff |
annotate
|
| Thu, 10 Jun 1999 10:35:58 +0200 |
paulson |
new preficates refl, sym [from Integ/Equiv], antisym
|
file |
diff |
annotate
|
| Wed, 02 Dec 1998 15:52:39 +0100 |
paulson |
new theorems Domain_Union, Range_Union
|
file |
diff |
annotate
|
| Tue, 01 Dec 1998 10:39:02 +0100 |
paulson |
better version of Image_diag
|
file |
diff |
annotate
|
| Mon, 30 Nov 1998 10:43:35 +0100 |
paulson |
new theorems about diag
|
file |
diff |
annotate
|
| Fri, 27 Nov 1998 10:40:29 +0100 |
paulson |
moved diag (diagonal relation) from Univ to Relation
|
file |
diff |
annotate
|
| Mon, 09 Nov 1998 11:00:44 +0100 |
paulson |
new Domain/Range rules
|
file |
diff |
annotate
|
| Thu, 15 Oct 1998 11:38:39 +0200 |
paulson |
Uses overload_1st_set to specify overloading
|
file |
diff |
annotate
|
| Fri, 02 Oct 1998 14:28:39 +0200 |
nipkow |
id <-> Id
|
file |
diff |
annotate
|
| Wed, 19 Aug 1998 10:27:00 +0200 |
paulson |
Overloading decl should assist Blast_tac
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 31 Jul 1998 18:46:28 +0200 |
paulson |
new theorems for partial funcs
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 14:19:02 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Mon, 27 Apr 1998 16:45:11 +0200 |
nipkow |
Added a few lemmas.
|
file |
diff |
annotate
|
| Mon, 30 Mar 1998 21:05:25 +0200 |
oheimb |
added introduction and elimination rules for Univalent
|
file |
diff |
annotate
|
| Mon, 16 Mar 1998 16:50:50 +0100 |
paulson |
inverse -> converse
|
file |
diff |
annotate
|
| Wed, 11 Mar 1998 11:05:14 +0100 |
paulson |
New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
|
file |
diff |
annotate
|
| Tue, 03 Mar 1998 15:12:25 +0100 |
paulson |
New theorems; tidied
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:48:04 +0100 |
oheimb |
added split_all_tac to claset()
|
file |
diff |
annotate
|
| Mon, 23 Feb 1998 11:15:40 +0100 |
paulson |
New laws for id
|
file |
diff |
annotate
|
| Thu, 05 Feb 1998 10:48:43 +0100 |
paulson |
New theorem Image_id
|
file |
diff |
annotate
|
| Mon, 02 Feb 1998 12:55:39 +0100 |
paulson |
Three new facts about Image
|
file |
diff |
annotate
|
| Tue, 16 Dec 1997 17:58:03 +0100 |
wenzelm |
expandshort;
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 26 Sep 1997 10:21:14 +0200 |
paulson |
Minor tidying to use Clarify_tac, etc.
|
file |
diff |
annotate
|
| Tue, 17 Jun 1997 09:01:56 +0200 |
nipkow |
converse -> ^-1
|
file |
diff |
annotate
|
| Thu, 05 Jun 1997 14:39:22 +0200 |
nipkow |
Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
|
file |
diff |
annotate
|
| 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
|