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
|