| Fri, 15 Sep 2000 12:39:57 +0200 |
paulson |
renamed (most of...) the select rules
|
file |
diff |
annotate
|
| Mon, 24 Jul 2000 23:51:46 +0200 |
wenzelm |
avoid referencing thy value;
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 10:42:14 +0200 |
paulson |
tidied a monstrous proof
|
file |
diff |
annotate
|
| Thu, 22 Jun 2000 23:04:34 +0200 |
wenzelm |
bind_thm(s);
|
file |
diff |
annotate
|
| Thu, 04 May 2000 15:14:56 +0200 |
paulson |
Suc 0 -> 1
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:19:37 +0200 |
paulson |
stopped using the obsolete "nat_ind_tac"
|
file |
diff |
annotate
|
| Thu, 13 Apr 2000 15:01:50 +0200 |
nipkow |
Times -> <*>
|
file |
diff |
annotate
|
| Thu, 24 Feb 2000 15:59:44 +0100 |
wenzelm |
workaround res_inst_tac/lift_inst_rule bug by explicit type contraint;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2000 11:06:03 +0100 |
paulson |
tidied parentheses
|
file |
diff |
annotate
|
| Wed, 18 Aug 1999 16:12:20 +0200 |
berghofe |
Eliminated some infixes.
|
file |
diff |
annotate
|
| Tue, 27 Jul 1999 10:30:26 +0200 |
paulson |
expandshort; tidied
|
file |
diff |
annotate
|
| Fri, 16 Jul 1999 12:09:48 +0200 |
berghofe |
Added some definitions and theorems needed for the
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 13:26:07 +0100 |
paulson |
inj is now a translation of inj_on
|
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 10:58:49 +0100 |
paulson |
removed obsolete comment and "open" declaration
|
file |
diff |
annotate
|
| Mon, 02 Nov 1998 15:31:29 +0100 |
paulson |
Domain r, Range r replace fst``r, snd``r
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 13:39:47 +0200 |
berghofe |
Renamed '$' to 'Scons' because of clashes with constants of the same
|
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
|
| Thu, 08 Jan 1998 18:09:07 +0100 |
oheimb |
added select_equality to the implicit claset
|
file |
diff |
annotate
|
| Thu, 08 Jan 1998 11:21:45 +0100 |
paulson |
Tidied by adding more default simprules
|
file |
diff |
annotate
|
| Wed, 03 Dec 1997 17:25:43 +0100 |
nipkow |
Replaced n ~= 0 by 0 < n
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 13:28:40 +0200 |
paulson |
Removed a few redundant additions of simprules or classical rules
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 10:21:10 +0200 |
paulson |
New facts about In0/1 by Burkhart Wolff
|
file |
diff |
annotate
|
| Tue, 15 Apr 1997 10:17:15 +0200 |
paulson |
Removed "AddSDs [Scons_inject];" because
|
file |
diff |
annotate
|
| 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 11:18:52 +0200 |
paulson |
Calls Blast_tac
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:40:05 +0200 |
paulson |
Tidied many proofs, using AddIffs to let equivalences take
|
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
|
| 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:45:01 +0200 |
paulson |
Using new "Times" infix
|
file |
diff |
annotate
|
| Mon, 11 Mar 1996 14:08:09 +0100 |
paulson |
New, one-line proof of inj_Atom
|
file |
diff |
annotate
|
| Mon, 04 Mar 1996 14:37:33 +0100 |
nipkow |
Added a constant UNIV == {x.True}
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:18 +0100 |
nipkow |
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:10:03 +0100 |
clasohm |
added local simpsets; removed IOA from 'make test'
|
file |
diff |
annotate
|
| Tue, 28 Mar 1995 12:21:10 +0200 |
clasohm |
renamed theorem "apfst" to "apfst_conv" to avoid conflict with function
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|